diff --git a/documentation/cli/03_build.md b/documentation/cli/03_build.md
index 4ce327d16..463467a80 100644
--- a/documentation/cli/03_build.md
+++ b/documentation/cli/03_build.md
@@ -59,6 +59,11 @@ The build also generates an **ABI file** at `build/abi.json` describing your pro
     The network to deploy to. Overrides the `NETWORK` environment variable.
 --endpoint <ENDPOINT>
     The endpoint to deploy to. Overrides the `ENDPOINT` environment variable.
+--network-retries <N>
+    Number of times to retry a network request on transient transport failure, with
+    exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the
+    NETWORK_RETRIES environment variable. Defaults to 2. HTTP errors and broadcast
+    calls are not retried.
 --devnet
     Whether the network is a devnet. If not set, defaults to the `DEVNET` environment variable.
 --consensus-heights <CONSENSUS_HEIGHTS>
diff --git a/documentation/cli/06_deploy.md b/documentation/cli/06_deploy.md
index 9d3b460ea..eba4a0534 100644
--- a/documentation/cli/06_deploy.md
+++ b/documentation/cli/06_deploy.md
@@ -135,6 +135,10 @@ The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set man
 
 <!-- markdown-link-check-enable -->
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 #### `--devnet`
 
 Specifies whether the network being deployed to is a devnet. If not set, defaults to the `DEVNET` environment variable.
diff --git a/documentation/cli/08_execute.md b/documentation/cli/08_execute.md
index d576dd0ff..bc87b2465 100644
--- a/documentation/cli/08_execute.md
+++ b/documentation/cli/08_execute.md
@@ -105,6 +105,10 @@ The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set man
 
 <!-- markdown-link-check-enable -->
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 #### `--devnet`
 
 Specifies whether the network being deployed to is a devnet. If not set, defaults to the `DEVNET` environment variable.
diff --git a/documentation/cli/10_query.md b/documentation/cli/10_query.md
index 63a636874..d0005c4ef 100644
--- a/documentation/cli/10_query.md
+++ b/documentation/cli/10_query.md
@@ -56,6 +56,10 @@ Specifies the network to deploy to. Overrides any `NETWORK` environment variable
 
 The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set manually or in a `.env` file.
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 #### `--latest`
 
 #### `-l`
@@ -132,6 +136,10 @@ Specifies the network to deploy to. Overrides any `NETWORK` environment variable
 
 The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set manually or in a `.env` file.
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 #### `--confirmed`
 
 #### `-c`
@@ -194,6 +202,10 @@ Specifies the network to deploy to. Overrides any `NETWORK` environment variable
 
 The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set manually or in a `.env` file.
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 #### `--mappings`
 
 Lists all mappings defined in the latest deployed edition of the program.
@@ -224,6 +236,10 @@ Specifies the network to deploy to. Overrides any `NETWORK` environment variable
 
 The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set manually or in a `.env` file.
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 ---
 
 ## `leo query committee`
@@ -240,6 +256,10 @@ Specifies the network to deploy to. Overrides any `NETWORK` environment variable
 
 The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set manually or in a `.env` file.
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 ---
 
 ## `leo query mempool`
@@ -280,6 +300,10 @@ Specifies the network to deploy to. Overrides any `NETWORK` environment variable
 
 The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set manually or in a `.env` file.
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 ---
 
 ## `leo query peers`
@@ -311,3 +335,7 @@ Specifies the network to deploy to. Overrides any `NETWORK` environment variable
 #### `--endpoint <ENDPOINT>`
 
 The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set manually or in a `.env` file.
+
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
diff --git a/documentation/cli/12_run.md b/documentation/cli/12_run.md
index 8c1f31742..e498880eb 100644
--- a/documentation/cli/12_run.md
+++ b/documentation/cli/12_run.md
@@ -78,6 +78,11 @@ leo run <FUNCTION_NAME> -- <INPUT_0> -- <INPUT_1> ...
     The network to deploy to. Overrides the `NETWORK` environment variable.
 --endpoint <ENDPOINT>
     The endpoint to deploy to. Overrides the `ENDPOINT` environment variable.
+--network-retries <N>
+    Number of times to retry a network request on transient transport failure, with
+    exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the
+    NETWORK_RETRIES environment variable. Defaults to 2. HTTP errors and broadcast
+    calls are not retried.
 --devnet
     Whether the network is a devnet. If not set, defaults to the `DEVNET` environment variable.
 --consensus-heights <CONSENSUS_HEIGHTS>
diff --git a/documentation/cli/15_upgrade.md b/documentation/cli/15_upgrade.md
index 504015a92..f0eb1629c 100644
--- a/documentation/cli/15_upgrade.md
+++ b/documentation/cli/15_upgrade.md
@@ -40,6 +40,10 @@ The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set man
 
 <!-- markdown-link-check-enable -->
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 #### `--devnet`
 
 Specifies whether the network being deployed to is a devnet. If not set, defaults to the `DEVNET` environment variable.
diff --git a/documentation/cli/16_synthesize.md b/documentation/cli/16_synthesize.md
index de0e91364..e2b506d7c 100644
--- a/documentation/cli/16_synthesize.md
+++ b/documentation/cli/16_synthesize.md
@@ -37,6 +37,10 @@ Specifies the network to deploy to. Overrides any `NETWORK` environment variable
 
 The endpoint to deploy to. Overrides any `ENDPOINT` environment variable set manually or in a `.env` file.
 
+#### `--network-retries <N>`
+
+Number of times to retry a network request on transient transport failure, with exponential backoff (1 s, 2 s, 4 s, … capped at 64 s). Overrides the `NETWORK_RETRIES` environment variable. Defaults to `2`. HTTP errors (4xx/5xx) and broadcast calls are not retried.
+
 #### `--local`
 
 #### `-l`
diff --git a/documentation/language/01_layout.md b/documentation/language/01_layout.md
index 7901efb66..615889a94 100644
--- a/documentation/language/01_layout.md
+++ b/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
diff --git a/documentation/language/06_libraries.md b/documentation/language/06_libraries.md
index 01141a9a8..1d4e51ad3 100644
--- a/documentation/language/06_libraries.md
+++ b/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 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
+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.
diff --git a/documentation/language/programs_in_practice/functions.md b/documentation/language/programs_in_practice/functions.md
index e713424f3..341cb8143 100644
--- a/documentation/language/programs_in_practice/functions.md
+++ b/documentation/language/programs_in_practice/functions.md
@@ -151,6 +151,10 @@ program main.aleo {
 
 Acceptable types for const generic parameters include integer types, `bool`, `scalar`, `group`, `field`, and `address`.
 
+:::note
+Const generic parameters are only valid on inlinable helper `fn` functions. They are not permitted on entry point functions inside a `program {}` block, `final fn` functions, functions annotated with `@no_inline`, or function signatures declared inside an `interface`.
+:::
+
 ### The `@no_inline` Annotation
 
 By default the compiler inlines helper functions that are called only once, which reduces call overhead. To prevent this, annotate the function with `@no_inline`:
diff --git a/documentation/language/programs_in_practice/interfaces.md b/documentation/language/programs_in_practice/interfaces.md
index 8eea9a2dd..08de3f483 100644
--- a/documentation/language/programs_in_practice/interfaces.md
+++ b/documentation/language/programs_in_practice/interfaces.md
@@ -19,7 +19,8 @@ program must provide. Interfaces are a compile-time concept and have no impact o
 They are only useful as a way to enforce structural contracts — ensuring that any program claiming to implement
 an interface actually provides all required functions, records, mappings, and storage variables — and to enable
 dynamic calls, where the caller knows *what* it can call without knowing *which* program it is calling at
-runtime. Interfaces are declared outside the `program {}` block or in a submodule.
+runtime. Interfaces can be declared outside the `program {}` block, in a submodule, or in a library package 
+(including library submodules).
 
 ```leo
 interface Transfer {
@@ -187,6 +188,136 @@ 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.
+
+`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 {
+    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 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
+
+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.
+
+`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 {
+    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:
diff --git a/documentation/language/programs_in_practice/intrinsics.md b/documentation/language/programs_in_practice/intrinsics.md
new file mode 100644
index 000000000..f0ba13b9e
--- /dev/null
+++ b/documentation/language/programs_in_practice/intrinsics.md
@@ -0,0 +1,212 @@
+---
+id: intrinsics
+title: Intrinsics
+sidebar_label: Intrinsics
+---
+
+[general tags]: # "intrinsic, dynamic_call, dynamic_contains, dynamic_get, dynamic_get_or_use, dynamic_dispatch, finalize"
+
+Intrinsics are low-level operations built into the compiler. They complement Leo's high-level abstractions and are useful when those abstractions aren't expressive enough for a particular use case. They are prefixed with `_` to make them visually distinct from user-defined functions.
+
+---
+
+## `_dynamic_call`
+
+Calls a function on a remote program determined at runtime, without requiring an interface definition. The target program, network, and function name are supplied as runtime values, and the full type signature is declared in the generic type parameters.
+
+Only valid in transition contexts — it cannot be used inside `final fn` functions or `final {}` blocks.
+
+### Syntax
+
+```
+_dynamic_call::[TYPE_PARAMS](prog, net, func, ...args)
+```
+
+- `prog` — the target program name, as a value of type `identifier` or a `field` representing an identifier
+- `net` — the network, as a value of type `identifier` or a `field` representing an identifier; currently only `'aleo'` is valid
+- `func` — the function name to call, as a value of type `identifier` or a `field` representing an identifier
+- `...args` — the function arguments, matching the input types declared in `TYPE_PARAMS`
+
+### Type parameters
+
+Type parameters follow one rule: **the last entry is the return type; all preceding entries are input types** with an optional visibility modifier (`public` or `private`). Omitting type parameters entirely means void return with compiler-inferred input visibility.
+
+#### No type parameters — void return
+
+```leo
+_dynamic_call(prog, net, func, x);
+```
+
+#### Return type only — inputs are `private` by default
+
+```leo
+let result: u64 = _dynamic_call::[u64](prog, net, func, x);
+```
+
+#### Explicit input visibility
+
+All type params before the last are input types. Each can carry a visibility modifier:
+
+```leo
+// One public input, then the return type
+let result: u64 = _dynamic_call::[public u64, u64](prog, net, func, x);
+```
+
+#### Multiple inputs
+
+```leo
+let (a, b): (u32, u32) = _dynamic_call::[public u32, public u32, (u32, u32)](prog, net, func, x, y);
+```
+
+#### Void return with input annotations
+
+Use `()` as the return type:
+
+```leo
+_dynamic_call::[public u64, ()](prog, net, func, x);
+```
+
+#### `Final` return
+
+When the called function returns a `Final`, include it in a tuple:
+
+```leo
+let (val, f): (u32, Final) = _dynamic_call::[(u32, Final)](target, 'aleo', 'increment', val);
+return (val, final {
+    f.run();
+});
+```
+
+#### `dyn record` inputs and outputs
+
+```leo
+let result: dyn record = _dynamic_call::[dyn record, dyn record](prog, net, func, token);
+```
+
+### Restrictions
+
+`_dynamic_call` is **not** allowed in `final fn` functions or `final {}` blocks.
+
+---
+
+## `_dynamic_contains`
+
+Checks whether a key exists in a mapping belonging to another program, determined at runtime. Only valid inside `final fn` functions or `final {}` blocks.
+
+### Syntax
+
+```leo
+let exists: bool = _dynamic_contains(prog, net, mapping, key);
+```
+
+- `prog` — the target program name, as a value of type `identifier` or a `field` representing an identifier
+- `net` — the network, as a value of type `identifier` or a `field` representing an identifier; currently only `'aleo'` is valid
+- `mapping` — the mapping name on the target program, as a value of type `identifier` or a `field` representing an identifier
+- `key` — a value whose type matches the target mapping's key type
+
+Returns `true` if `key` is present, `false` otherwise.
+
+### Example
+
+```leo showLineNumbers
+program checker.aleo {
+    mapping seen: address => bool;
+
+    fn check(prog: field, net: field, map: field, key: address) -> Final {
+        return final { finalize_check(prog, net, map, key); };
+    }
+
+    @noupgrade
+    constructor() {}
+}
+
+final fn finalize_check(prog: field, net: field, map: field, key: address) {
+    let exists: bool = _dynamic_contains(prog, net, map, key);
+    Mapping::set(seen, key, exists);
+}
+```
+
+---
+
+## `_dynamic_get`
+
+Reads a value from a mapping belonging to another program, determined at runtime. Only valid inside `final fn` functions or `final {}` blocks.
+
+Fails at runtime if the key is not present — use [`_dynamic_get_or_use`](#_dynamic_get_or_use) when the key may be absent.
+
+### Syntax
+
+```leo
+let val: T = _dynamic_get::[T](prog, net, mapping, key);
+```
+
+- `prog` — the target program name, as a value of type `identifier` or a `field` representing an identifier
+- `net` — the network, as a value of type `identifier` or a `field` representing an identifier; currently only `'aleo'` is valid
+- `mapping` — the mapping name on the target program, as a value of type `identifier` or a `field` representing an identifier
+- `key` — a value whose type matches the target mapping's key type
+- `T` — must match the target mapping's value type
+
+### Example
+
+```leo showLineNumbers
+program reader.aleo {
+    mapping result: address => u64;
+
+    fn read(prog: field, net: field, map: field, key: address) -> Final {
+        return final { finalize_read(prog, net, map, key); };
+    }
+
+    @noupgrade
+    constructor() {}
+}
+
+final fn finalize_read(prog: field, net: field, map: field, key: address) {
+    let val: u64 = _dynamic_get::[u64](prog, net, map, key);
+    Mapping::set(result, key, val);
+}
+```
+
+For example, using identifier literals:
+
+```leo
+let val: u64 = _dynamic_get::[u64]('some_program', 'aleo', 'balances', key);
+```
+
+---
+
+## `_dynamic_get_or_use`
+
+Reads a value from a mapping belonging to another program, determined at runtime, returning a default value if the key is absent. Only valid inside `final fn` functions or `final {}` blocks.
+
+### Syntax
+
+```leo
+let val: T = _dynamic_get_or_use::[T](prog, net, mapping, key, default);
+```
+
+- `prog` — the target program name, as a value of type `identifier` or a `field` representing an identifier
+- `net` — the network, as a value of type `identifier` or a `field` representing an identifier; currently only `'aleo'` is valid
+- `mapping` — the mapping name on the target program, as a value of type `identifier` or a `field` representing an identifier
+- `key` — a value whose type matches the target mapping's key type
+- `default` — the fallback value returned when `key` is absent; must be the same type as `T`
+- `T` — must match the target mapping's value type
+
+### Example
+
+```leo showLineNumbers
+program reader.aleo {
+    mapping result: address => u64;
+
+    fn read(prog: field, net: field, map: field, key: address) -> Final {
+        return final { finalize_read(prog, net, map, key); };
+    }
+
+    @noupgrade
+    constructor() {}
+}
+
+final fn finalize_read(prog: field, net: field, map: field, key: address) {
+    let val: u64 = _dynamic_get_or_use::[u64](prog, net, map, key, 0u64);
+    Mapping::set(result, key, val);
+}
+```