Repository: aptos-labs/aptos-core (language: python)

Issue:
[compiler-v2] Generic TypeInfo verification broken
Consider code like:

```
module app::m {
    use aptos_stdlib::type_info;
    
    fun generic_type_info_verification_target<A>(): type_info::TypeInfo {
       type_info::type_of<A>()
    }
    spec generic_type_info_verification_target {
        ensures result == generic_type_info_verification_target<A>();
    }
}
```

This yields in the following Boogie compilation error:

```
Move prover returns: [internal] boogie exited with compilation errors:
type_reflection.bpl(5059,26): Error: cannot refer to a global variable in this context: #0_info
type_reflection.bpl(5059,38): Error: cannot refer to a global variable in this context: #0_info
type_reflection.bpl(5059,50): Error: cannot refer to a global variable in this context: #0_info
```

This seems to be a bug in the new specification function inferrer shared between compiler v1 and v2. The native function `type_info::type_of` cannot be called from a specification function as it refers to type reflection state `#0_info`. 


Discussion / hints:

Fix patch:
diff --git a/crates/aptos/CHANGELOG.md b/crates/aptos/CHANGELOG.md
index 9dd9d07837866..9395dabd2382c 100644
--- a/crates/aptos/CHANGELOG.md
+++ b/crates/aptos/CHANGELOG.md
@@ -3,6 +3,7 @@
 All notable changes to the Aptos CLI will be captured in this file. This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html) and the format set out by [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ## Unreleased
+- Fixes a bug in the Move Prover leading to internal error in generated boogie (error 'global `#0_info` cannot be accessed')
 
 ## [3.5.1] - 2024/07/21
 - Upgraded indexer processors for localnet from 5244b84fa5ed872e5280dc8df032d744d62ad29d to fa1ce4947f4c2be57529f1c9732529e05a06cb7f. Upgraded Hasura metadata accordingly.
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs b/third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs
index 5fd1f908654b8..1077b7b3af83e 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs
@@ -255,6 +255,7 @@ fn derive_spec_fun(env: &mut GlobalEnv, fun_id: QualifiedId<FunId>) -> Qualified
         body,
         callees: BTreeSet::new(),
         is_recursive: RefCell::new(None),
+        insts_using_generic_type_reflection: Default::default(),
     };
     env.add_spec_function_def(fun_id.module_id, decl)
 }
diff --git a/third_party/move/move-model/src/ast.rs b/third_party/move/move-model/src/ast.rs
index e06543c6fd668..9c488890f5322 100644
--- a/third_party/move/move-model/src/ast.rs
+++ b/third_party/move/move-model/src/ast.rs
@@ -60,6 +60,8 @@ pub struct SpecFunDecl {
     pub body: Option<Exp>,
     pub callees: BTreeSet<QualifiedInstId<SpecFunId>>,
     pub is_recursive: RefCell<Option<bool>>,
+    /// The instantiations for which this function is known to use generic type reflection.
+    pub insts_using_generic_type_reflection: RefCell<BTreeMap<Vec<Type>, bool>>,
 }
 
 // =================================================================================================
diff --git a/third_party/move/move-model/src/builder/module_builder.rs b/third_party/move/move-model/src/builder/module_builder.rs
index 9f381cc5337b2..6c673e6ea4a5a 100644
--- a/third_party/move/move-model/src/builder/module_builder.rs
+++ b/third_party/move/move-model/src/builder/module_builder.rs
@@ -763,6 +763,7 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
             body: None,
             callees: Default::default(),
             is_recursive: Default::default(),
+            insts_using_generic_type_reflection: Default::default(),
         };
         self.spec_funs.push(fun_decl);
     }
diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs
index 9d563f8a1fdda..c8e63797a45da 100644
--- a/third_party/move/move-model/src/model.rs
+++ b/third_party/move/move-model/src/model.rs
@@ -1372,6 +1372,81 @@ impl GlobalEnv {
         }
     }
 
+    /// Determines whether the given spec fun uses type reflection over type parameters.
+    pub fn spec_fun_uses_generic_type_reflection(
+        &self,
+        fun_id: &QualifiedInstId<SpecFunId>,
+    ) -> bool {
+        fn uses_generic_type_reflection(
+            env: &GlobalEnv,
+            visited: &mut BTreeSet<QualifiedInstId<SpecFunId>>,
+            fun: &QualifiedInstId<SpecFunId>,
+        ) -> bool {
+            if !visited.insert(fun.clone()) {
+                return false;
+            }
+            let module = env.get_module(fun.module_id);
+            let decl = module.get_spec_fun(fun.id);
+            if let Some(def) = &decl.body {
+                // Check called spec funs
+                def.called_spec_funs(env).into_iter().any(|qid| {
+                    let qid_inst = qid.instantiate(&fun.inst);
+                    is_generic_type_reflection(env, &qid_inst)
+                        || uses_generic_type_reflection(env, visited, &qid_inst)
+                })
+            } else {
+                false
+            }
+        }
+        fn is_generic_type_reflection(
+            env: &GlobalEnv,
+            fun_id: &QualifiedInstId<SpecFunId>,
+        ) -> bool {
+            static REFLECTION_FUNS: Lazy<BTreeSet<String>> = Lazy::new(|| {
+                [
+                    well_known::TYPE_INFO_SPEC.to_owned(),
+                    well_known::TYPE_NAME_SPEC.to_owned(),
+                    well_known::TYPE_NAME_GET_SPEC.to_owned(),
+                ]
+                .into_iter()
+                .collect()
+            });
+            // The function must be at `extlib` or `stdlib`.
+            let module = env.get_module(fun_id.module_id);
+            let addr = module.get_name().addr();
+            if addr == &env.get_extlib_address() || addr == &env.get_stdlib_address() {
+                let fun = module.get_spec_fun(fun_id.id);
+                let name = format!(
+                    "{}::{}",
+                    module.get_name().name().display(module.symbol_pool()),
+                    fun.name.display(module.symbol_pool())
+                );
+                REFLECTION_FUNS.contains(&name)
+                    && fun_id.inst.iter().any(|ty| ty.is_type_parameter())
+            } else {
+                false
+            }
+        }
+        let module = self.get_module(fun_id.module_id);
+        let decl = module.get_spec_fun(fun_id.id);
+        let uses = decl
+            .insts_using_generic_type_reflection
+            .borrow()
+            .get(&fun_id.inst)
+            .cloned();
+        if let Some(b) = uses {
+            b
+        } else {
+            let b = uses_generic_type_reflection(self, &mut BTreeSet::new(), fun_id);
+            module
+                .get_spec_fun(fun_id.id)
+                .insts_using_generic_type_reflection
+                .borrow_mut()
+                .insert(fun_id.inst.clone(), b);
+            b
+        }
+    }
+
     /// Returns true if the type represents the well-known event handle type.
     pub fn is_wellknown_event_handle_type(&self, ty: &Type) -> bool {
         if let Type::Struct(mid, sid, _) = ty {
@@ -4771,6 +4846,15 @@ impl GetNameString for QualifiedId<FunId> {
     }
 }
 
+impl GetNameString for QualifiedId<SpecFunId> {
+    fn get_name_for_display(&self, env: &GlobalEnv) -> String {
+        env.get_spec_fun(*self)
+            .name
+            .display(env.symbol_pool())
+            .to_string()
+    }
+}
+
 impl<'a, Id: Clone> fmt::Display for EnvDisplay<'a, QualifiedId<Id>>
 where
     QualifiedId<Id>: GetNameString,
diff --git a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
index fc78a5f833fc4..9d84ff64e72e0 100644
--- a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
@@ -274,9 +274,11 @@ impl<'env> SpecTranslator<'env> {
             self.error(&fun.loc, "function or tuple result type not yet supported");
             return;
         }
-        let recursive = self
+        let qid = module_env.get_id().qualified(id);
+        let recursive = self.env.is_spec_fun_recursive(qid);
+        let type_reflection = self
             .env
-            .is_spec_fun_recursive(module_env.get_id().qualified(id));
+            .spec_fun_uses_generic_type_reflection(&qid.instantiate(self.type_inst.clone()));
         emitln!(
             self.writer,
             "// {}spec fun {}",
@@ -307,6 +309,18 @@ impl<'env> SpecTranslator<'env> {
                 boogie_type
             }
         };
+        let type_info_params = if type_reflection {
+            (0..fun.type_params.len())
+                .map(|i| {
+                    format!(
+                        "{}_info: $TypeParamInfo",
+                        boogie_type(self.env, &Type::TypeParameter(i as u16))
+                    )
+                })
+                .collect_vec()
+        } else {
+            vec![]
+        };
         let result_type = ty_str_fn(bv_flag_result)(self.env, &self.inst(&fun.result_type));
         // it is possible that the spec fun may refer to the same memory after monomorphization,
         // (e.g., one via concrete type and the other via type parameter being instantiated).
@@ -352,7 +366,10 @@ impl<'env> SpecTranslator<'env> {
             });
         self.writer.set_location(&fun.loc);
         let boogie_name = boogie_spec_fun_name(module_env, id, &self.type_inst, bv_flag_result);
-        let param_list = mem_params.chain(params).join(", ");
+        let param_list = type_info_params
+            .into_iter()
+            .chain(mem_params.chain(params))
+            .join(", ");
         let attrs = if fun.uninterpreted || recursive {
             ""
         } else {
@@ -1031,14 +1048,69 @@ impl<'env> SpecTranslator<'env> {
         let inst = &self.get_node_instantiation(node_id);
         let module_env = &self.env.get_module(module_id);
         let fun_decl = module_env.get_spec_fun(fun_id);
+        if self.try_translate_spec_fun_reflection_call(module_env, fun_decl, inst) {
+            return;
+        }
+
+        // regular path
         let global_state = &self
             .env
             .get_extension::<GlobalNumberOperationState>()
             .expect("global number operation state");
+        let is_vector_table_module = module_env.is_std_vector() || module_env.is_table();
+        let bv_flag = if is_vector_table_module && !args.is_empty() {
+            global_state.get_node_num_oper(args[0].node_id()) == Bitwise
+        } else {
+            global_state.get_node_num_oper(node_id) == Bitwise
+        };
+        let name = boogie_spec_fun_name(module_env, fun_id, inst, bv_flag);
+        emit!(self.writer, "{}(", name);
+        let mut first = true;
+        let mut maybe_comma = || {
+            if first {
+                first = false;
+            } else {
+                emit!(self.writer, ", ");
+            }
+        };
+        // Start with type info parameters
+        if self
+            .env
+            .spec_fun_uses_generic_type_reflection(&module_id.qualified_inst(fun_id, inst.clone()))
+        {
+            for i in 0..fun_decl.type_params.len() {
+                maybe_comma();
+                emit!(
+                    self.writer,
+                    "{}_info",
+                    boogie_type(self.env, &Type::TypeParameter(i as u16))
+                )
+            }
+        }
+        // Add memory parameters.
+        let label_at = |i| memory_labels.as_ref().map(|labels| labels[i]);
+        let mut i = 0;
+        for memory in &fun_decl.used_memory {
+            let memory = &memory.to_owned().instantiate(inst);
+            maybe_comma();
+            let memory = boogie_resource_memory_name(self.env, memory, &label_at(i));
+            emit!(self.writer, &memory);
+            i = usize::saturating_add(i, 1);
+        }
+        // Finally add argument expressions
+        for exp in args {
+            maybe_comma();
+            self.translate_exp(exp);
+        }
+        emit!(self.writer, ")");
+    }
 
-        // special casing for type reflection
-        let mut processed = false;
-
+    fn try_translate_spec_fun_reflection_call(
+        &self,
+        module_env: &ModuleEnv,
+        fun_decl: &SpecFunDecl,
+        inst: &[Type],
+    ) -> bool {
         // TODO(mengxu): change it to a better address name instead of extlib
         if self.env.get_extlib_address() == *module_env.get_name().addr() {
             let qualified_name = format!(
@@ -1053,7 +1125,7 @@ impl<'env> SpecTranslator<'env> {
                     "{}",
                     boogie_reflection_type_name(self.env, &inst[0], false)
                 );
-                processed = true;
+                true
             } else if qualified_name == TYPE_INFO_SPEC {
                 assert_eq!(inst.len(), 1);
                 // TODO(mengxu): by ignoring the first return value of this function, we are
@@ -1061,7 +1133,7 @@ impl<'env> SpecTranslator<'env> {
                 // invoking `type_info` on a primitive type like: `type_info<bool>`.
                 let (_, info) = boogie_reflection_type_info(self.env, &inst[0]);
                 emit!(self.writer, "{}", info);
-                processed = true;
+                true
             } else if qualified_name == TYPE_SPEC_IS_STRUCT {
                 assert_eq!(inst.len(), 1);
                 emit!(
@@ -1069,11 +1141,11 @@ impl<'env> SpecTranslator<'env> {
                     "{}",
                     boogie_reflection_type_is_struct(self.env, &inst[0])
                 );
-                processed = true;
+                true
+            } else {
+                false
             }
-        }
-
-        if self.env.get_stdlib_address() == *module_env.get_name().addr() {
+        } else if self.env.get_stdlib_address() == *module_env.get_name().addr() {
             let qualified_name = format!(
                 "{}::{}",
                 module_env.get_name().name().display(self.env.symbol_pool()),
@@ -1086,42 +1158,12 @@ impl<'env> SpecTranslator<'env> {
                     "{}",
                     boogie_reflection_type_name(self.env, &inst[0], true)
                 );
-                processed = true;
-            }
-        }
-
-        let is_vector_table_module = module_env.is_std_vector() || module_env.is_table();
-        // regular path
-        if !processed {
-            let bv_flag = if is_vector_table_module && !args.is_empty() {
-                global_state.get_node_num_oper(args[0].node_id()) == Bitwise
+                true
             } else {
-                global_state.get_node_num_oper(node_id) == Bitwise
-            };
-            let name = boogie_spec_fun_name(module_env, fun_id, inst, bv_flag);
-            emit!(self.writer, "{}(", name);
-            let mut first = true;
-            let mut maybe_comma = || {
-                if first {
-                    first = false;
-                } else {
-                    emit!(self.writer, ", ");
-                }
-            };
-            let label_at = |i| memory_labels.as_ref().map(|labels| labels[i]);
-            let mut i = 0;
-            for memory in &fun_decl.used_memory {
-                let memory = &memory.to_owned().instantiate(inst);
-                maybe_comma();
-                let memory = boogie_resource_memory_name(self.env, memory, &label_at(i));
-                emit!(self.writer, &memory);
-                i = usize::saturating_add(i, 1);
+                false
             }
-            for exp in args {
-                maybe_comma();
-                self.translate_exp(exp);
-            }
-            emit!(self.writer, ")");
+        } else {
+            false
         }
     }
 


Test patch:
diff --git a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/aggregator_v2.md b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/aggregator_v2.md
index 2318d57e73b9a..70e859a72b509 100644
--- a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/aggregator_v2.md
+++ b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/aggregator_v2.md
@@ -58,6 +58,10 @@ read, read_snapshot, read_derived_string
     -  [Function `read`](#@Specification_1_read)
     -  [Function `snapshot`](#@Specification_1_snapshot)
     -  [Function `create_snapshot`](#@Specification_1_create_snapshot)
+    -  [Function `read_snapshot`](#@Specification_1_read_snapshot)
+    -  [Function `read_derived_string`](#@Specification_1_read_derived_string)
+    -  [Function `create_derived_string`](#@Specification_1_create_derived_string)
+    -  [Function `derive_string_concat`](#@Specification_1_derive_string_concat)
     -  [Function `copy_snapshot`](#@Specification_1_copy_snapshot)
     -  [Function `string_concat`](#@Specification_1_string_concat)
 
@@ -902,6 +906,70 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
+<pre><code><b>pragma</b> opaque;
+</code></pre>
+
+
+
+<a id="@Specification_1_read_snapshot"></a>
+
+### Function `read_snapshot`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="aggregator_v2.md#0x1_aggregator_v2_read_snapshot">read_snapshot</a>&lt;IntElement&gt;(snapshot: &<a href="aggregator_v2.md#0x1_aggregator_v2_AggregatorSnapshot">aggregator_v2::AggregatorSnapshot</a>&lt;IntElement&gt;): IntElement
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> opaque;
+</code></pre>
+
+
+
+<a id="@Specification_1_read_derived_string"></a>
+
+### Function `read_derived_string`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="aggregator_v2.md#0x1_aggregator_v2_read_derived_string">read_derived_string</a>(snapshot: &<a href="aggregator_v2.md#0x1_aggregator_v2_DerivedStringSnapshot">aggregator_v2::DerivedStringSnapshot</a>): <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/string.md#0x1_string_String">string::String</a>
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> opaque;
+</code></pre>
+
+
+
+<a id="@Specification_1_create_derived_string"></a>
+
+### Function `create_derived_string`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="aggregator_v2.md#0x1_aggregator_v2_create_derived_string">create_derived_string</a>(value: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/string.md#0x1_string_String">string::String</a>): <a href="aggregator_v2.md#0x1_aggregator_v2_DerivedStringSnapshot">aggregator_v2::DerivedStringSnapshot</a>
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> opaque;
+</code></pre>
+
+
+
+<a id="@Specification_1_derive_string_concat"></a>
+
+### Function `derive_string_concat`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="aggregator_v2.md#0x1_aggregator_v2_derive_string_concat">derive_string_concat</a>&lt;IntElement&gt;(before: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/string.md#0x1_string_String">string::String</a>, snapshot: &<a href="aggregator_v2.md#0x1_aggregator_v2_AggregatorSnapshot">aggregator_v2::AggregatorSnapshot</a>&lt;IntElement&gt;, after: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/string.md#0x1_string_String">string::String</a>): <a href="aggregator_v2.md#0x1_aggregator_v2_DerivedStringSnapshot">aggregator_v2::DerivedStringSnapshot</a>
+</code></pre>
+
+
+
+
 <pre><code><b>pragma</b> opaque;
 </code></pre>
 
diff --git a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/code.md b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/code.md
index b3adf637e2702..2f51dad607837 100644
--- a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/code.md
+++ b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/code.md
@@ -94,7 +94,7 @@ The package registry at the given address.
 Metadata for a package. All byte blobs are represented as base64-of-gzipped-bytes
 
 
-<pre><code><b>struct</b> <a href="code.md#0x1_code_PackageMetadata">PackageMetadata</a> <b>has</b> drop, store
+<pre><code><b>struct</b> <a href="code.md#0x1_code_PackageMetadata">PackageMetadata</a> <b>has</b> <b>copy</b>, drop, store
 </code></pre>
 
 
@@ -200,7 +200,7 @@ A dependency to a package published at address
 Metadata about a module in a package.
 
 
-<pre><code><b>struct</b> <a href="code.md#0x1_code_ModuleMetadata">ModuleMetadata</a> <b>has</b> drop, store
+<pre><code><b>struct</b> <a href="code.md#0x1_code_ModuleMetadata">ModuleMetadata</a> <b>has</b> <b>copy</b>, drop, store
 </code></pre>
 
 
@@ -612,9 +612,9 @@ package.
     // Checks for valid dependencies <b>to</b> other packages
     <b>let</b> allowed_deps = <a href="code.md#0x1_code_check_dependencies">check_dependencies</a>(addr, &pack);
 
-    // Check package against conflicts
+    // Check <b>package</b> against conflicts
     // To avoid prover compiler <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error">error</a> on <b>spec</b>
-    // the package need <b>to</b> be an immutable variable
+    // the <b>package</b> need <b>to</b> be an immutable variable
     <b>let</b> module_names = <a href="code.md#0x1_code_get_module_names">get_module_names</a>(&pack);
     <b>let</b> package_immutable = &<b>borrow_global</b>&lt;<a href="code.md#0x1_code_PackageRegistry">PackageRegistry</a>&gt;(addr).packages;
     <b>let</b> len = <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector_length">vector::length</a>(package_immutable);
@@ -687,9 +687,17 @@ package.
     );
 
     <b>let</b> registry = <b>borrow_global_mut</b>&lt;<a href="code.md#0x1_code_PackageRegistry">PackageRegistry</a>&gt;(code_object_addr);
-    <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector_for_each_mut">vector::for_each_mut</a>&lt;<a href="code.md#0x1_code_PackageMetadata">PackageMetadata</a>&gt;(&<b>mut</b> registry.packages, |pack| {
-        <b>let</b> package: &<b>mut</b> <a href="code.md#0x1_code_PackageMetadata">PackageMetadata</a> = pack;
-        package.upgrade_policy = <a href="code.md#0x1_code_upgrade_policy_immutable">upgrade_policy_immutable</a>();
+    <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector_for_each_mut">vector::for_each_mut</a>(&<b>mut</b> registry.packages, |pack| {
+        <b>let</b> <b>package</b>: &<b>mut</b> <a href="code.md#0x1_code_PackageMetadata">PackageMetadata</a> = pack;
+        <b>package</b>.upgrade_policy = <a href="code.md#0x1_code_upgrade_policy_immutable">upgrade_policy_immutable</a>();
+    });
+
+    // We unfortunately have <b>to</b> make a <b>copy</b> of each <b>package</b> <b>to</b> avoid borrow checker issues <b>as</b> check_dependencies
+    // needs <b>to</b> borrow <a href="code.md#0x1_code_PackageRegistry">PackageRegistry</a> from the dependency packages.
+    // This would increase the amount of gas used, but this is a rare operation and it's rare <b>to</b> have many packages
+    // in a single <a href="code.md#0x1_code">code</a> <a href="object.md#0x1_object">object</a>.
+    <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector_for_each">vector::for_each</a>(registry.packages, |pack| {
+        <a href="code.md#0x1_code_check_dependencies">check_dependencies</a>(code_object_addr, &pack);
     });
 }
 </code></pre>
@@ -779,7 +787,7 @@ Checks whether a new package with given names can co-exist with old package.
 
 
 <pre><code><b>fun</b> <a href="code.md#0x1_code_check_coexistence">check_coexistence</a>(old_pack: &<a href="code.md#0x1_code_PackageMetadata">PackageMetadata</a>, new_modules: &<a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector">vector</a>&lt;String&gt;) {
-    // The modules introduced by each package must not overlap <b>with</b> `names`.
+    // The modules introduced by each <b>package</b> must not overlap <b>with</b> `names`.
     <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector_for_each_ref">vector::for_each_ref</a>(&old_pack.modules, |old_mod| {
         <b>let</b> old_mod: &<a href="code.md#0x1_code_ModuleMetadata">ModuleMetadata</a> = old_mod;
         <b>let</b> j = 0;
diff --git a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/coin.md b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/coin.md
index 146093ce9e8d6..f232014d2925e 100644
--- a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/coin.md
+++ b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/coin.md
@@ -1440,7 +1440,7 @@ Create APT pairing by passing <code>AptosCoin</code>.
             };
         <a href="primary_fungible_store.md#0x1_primary_fungible_store_create_primary_store_enabled_fungible_asset">primary_fungible_store::create_primary_store_enabled_fungible_asset</a>(
             &metadata_object_cref,
-            <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_map">option::map</a>(<a href="coin.md#0x1_coin_coin_supply">coin_supply</a>&lt;CoinType&gt;(), |_| <a href="coin.md#0x1_coin_MAX_U128">MAX_U128</a>),
+            <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_none">option::none</a>(),
             <a href="coin.md#0x1_coin_name">name</a>&lt;CoinType&gt;(),
             <a href="coin.md#0x1_coin_symbol">symbol</a>&lt;CoinType&gt;(),
             <a href="coin.md#0x1_coin_decimals">decimals</a>&lt;CoinType&gt;(),
@@ -4595,6 +4595,27 @@ The creator of <code>CoinType</code> must be <code>@aptos_framework</code>.
 </code></pre>
 
 
+Make sure <code>name</code> and <code>symbol</code> are legal length.
+Only the creator of <code>CoinType</code> can initialize.
+
+
+<a id="0x1_coin_InitializeInternalSchema"></a>
+
+
+<pre><code><b>schema</b> <a href="coin.md#0x1_coin_InitializeInternalSchema">InitializeInternalSchema</a>&lt;CoinType&gt; {
+    <a href="account.md#0x1_account">account</a>: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/signer.md#0x1_signer">signer</a>;
+    name: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;;
+    symbol: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;;
+    <b>let</b> account_addr = <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>);
+    <b>let</b> coin_address = <a href="../../../aptos-stdlib/tests/compiler-v2-doc/type_info.md#0x1_type_info_type_of">type_info::type_of</a>&lt;CoinType&gt;().account_address;
+    <b>aborts_if</b> coin_address != account_addr;
+    <b>aborts_if</b> <b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinInfo">CoinInfo</a>&lt;CoinType&gt;&gt;(account_addr);
+    <b>aborts_if</b> len(name) &gt; <a href="coin.md#0x1_coin_MAX_COIN_NAME_LENGTH">MAX_COIN_NAME_LENGTH</a>;
+    <b>aborts_if</b> len(symbol) &gt; <a href="coin.md#0x1_coin_MAX_COIN_SYMBOL_LENGTH">MAX_COIN_SYMBOL_LENGTH</a>;
+}
+</code></pre>
+
+
 
 <a id="@Specification_1_initialize_internal"></a>
 
diff --git a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/dispatchable_fungible_asset.md b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/dispatchable_fungible_asset.md
index c9a4a263f1a2a..dca680da9e6bc 100644
--- a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/dispatchable_fungible_asset.md
+++ b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/dispatchable_fungible_asset.md
@@ -23,19 +23,23 @@ See AIP-73 for further discussion
 -  [Resource `TransferRefStore`](#0x1_dispatchable_fungible_asset_TransferRefStore)
 -  [Constants](#@Constants_0)
 -  [Function `register_dispatch_functions`](#0x1_dispatchable_fungible_asset_register_dispatch_functions)
+-  [Function `register_derive_supply_dispatch_function`](#0x1_dispatchable_fungible_asset_register_derive_supply_dispatch_function)
 -  [Function `withdraw`](#0x1_dispatchable_fungible_asset_withdraw)
 -  [Function `deposit`](#0x1_dispatchable_fungible_asset_deposit)
 -  [Function `transfer`](#0x1_dispatchable_fungible_asset_transfer)
 -  [Function `transfer_assert_minimum_deposit`](#0x1_dispatchable_fungible_asset_transfer_assert_minimum_deposit)
 -  [Function `derived_balance`](#0x1_dispatchable_fungible_asset_derived_balance)
+-  [Function `derived_supply`](#0x1_dispatchable_fungible_asset_derived_supply)
 -  [Function `borrow_transfer_ref`](#0x1_dispatchable_fungible_asset_borrow_transfer_ref)
 -  [Function `dispatchable_withdraw`](#0x1_dispatchable_fungible_asset_dispatchable_withdraw)
 -  [Function `dispatchable_deposit`](#0x1_dispatchable_fungible_asset_dispatchable_deposit)
 -  [Function `dispatchable_derived_balance`](#0x1_dispatchable_fungible_asset_dispatchable_derived_balance)
+-  [Function `dispatchable_derived_supply`](#0x1_dispatchable_fungible_asset_dispatchable_derived_supply)
 -  [Specification](#@Specification_1)
     -  [Function `dispatchable_withdraw`](#@Specification_1_dispatchable_withdraw)
     -  [Function `dispatchable_deposit`](#@Specification_1_dispatchable_deposit)
     -  [Function `dispatchable_derived_balance`](#@Specification_1_dispatchable_derived_balance)
+    -  [Function `dispatchable_derived_supply`](#@Specification_1_dispatchable_derived_supply)
 
 
 <pre><code><b>use</b> <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error">0x1::error</a>;
@@ -160,6 +164,36 @@ TransferRefStore doesn't exist on the fungible asset type.
 
 
 
+</details>
+
+<a id="0x1_dispatchable_fungible_asset_register_derive_supply_dispatch_function"></a>
+
+## Function `register_derive_supply_dispatch_function`
+
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_register_derive_supply_dispatch_function">register_derive_supply_dispatch_function</a>(constructor_ref: &<a href="object.md#0x1_object_ConstructorRef">object::ConstructorRef</a>, dispatch_function: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_Option">option::Option</a>&lt;<a href="function_info.md#0x1_function_info_FunctionInfo">function_info::FunctionInfo</a>&gt;)
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_register_derive_supply_dispatch_function">register_derive_supply_dispatch_function</a>(
+    constructor_ref: &ConstructorRef,
+    dispatch_function: Option&lt;FunctionInfo&gt;
+) {
+    <a href="fungible_asset.md#0x1_fungible_asset_register_derive_supply_dispatch_function">fungible_asset::register_derive_supply_dispatch_function</a>(
+        constructor_ref,
+        dispatch_function
+    );
+}
+</code></pre>
+
+
+
 </details>
 
 <a id="0x1_dispatchable_fungible_asset_withdraw"></a>
@@ -364,6 +398,45 @@ The semantics of value will be governed by the function specified in DispatchFun
 
 
 
+</details>
+
+<a id="0x1_dispatchable_fungible_asset_derived_supply"></a>
+
+## Function `derived_supply`
+
+Get the derived supply of the fungible asset using the overloaded hook.
+
+The semantics of supply will be governed by the function specified in DeriveSupplyDispatch.
+
+
+<pre><code>#[view]
+<b>public</b> <b>fun</b> <a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_derived_supply">derived_supply</a>&lt;T: key&gt;(metadata: <a href="object.md#0x1_object_Object">object::Object</a>&lt;T&gt;): <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_Option">option::Option</a>&lt;u128&gt;
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_derived_supply">derived_supply</a>&lt;T: key&gt;(metadata: Object&lt;T&gt;): Option&lt;u128&gt; {
+    <b>let</b> func_opt = <a href="fungible_asset.md#0x1_fungible_asset_derived_supply_dispatch_function">fungible_asset::derived_supply_dispatch_function</a>(metadata);
+    <b>if</b> (<a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_is_some">option::is_some</a>(&func_opt)) {
+        <b>assert</b>!(
+            <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/features.md#0x1_features_dispatchable_fungible_asset_enabled">features::dispatchable_fungible_asset_enabled</a>(),
+            <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_aborted">error::aborted</a>(<a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_ENOT_ACTIVATED">ENOT_ACTIVATED</a>)
+        );
+        <b>let</b> func = <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_borrow">option::borrow</a>(&func_opt);
+        <a href="function_info.md#0x1_function_info_load_module_from_function">function_info::load_module_from_function</a>(func);
+        <a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_dispatchable_derived_supply">dispatchable_derived_supply</a>(metadata, func)
+    } <b>else</b> {
+        <a href="fungible_asset.md#0x1_fungible_asset_supply">fungible_asset::supply</a>(metadata)
+    }
+}
+</code></pre>
+
+
+
 </details>
 
 <a id="0x1_dispatchable_fungible_asset_borrow_transfer_ref"></a>
@@ -474,6 +547,31 @@ The semantics of value will be governed by the function specified in DispatchFun
 
 
 
+</details>
+
+<a id="0x1_dispatchable_fungible_asset_dispatchable_derived_supply"></a>
+
+## Function `dispatchable_derived_supply`
+
+
+
+<pre><code><b>fun</b> <a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_dispatchable_derived_supply">dispatchable_derived_supply</a>&lt;T: key&gt;(store: <a href="object.md#0x1_object_Object">object::Object</a>&lt;T&gt;, function: &<a href="function_info.md#0x1_function_info_FunctionInfo">function_info::FunctionInfo</a>): <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_Option">option::Option</a>&lt;u128&gt;
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>native</b> <b>fun</b> <a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_dispatchable_derived_supply">dispatchable_derived_supply</a>&lt;T: key&gt;(
+    store: Object&lt;T&gt;,
+    function: &FunctionInfo,
+): Option&lt;u128&gt;;
+</code></pre>
+
+
+
 </details>
 
 <a id="@Specification_1"></a>
@@ -530,6 +628,22 @@ The semantics of value will be governed by the function specified in DispatchFun
 
 
 
+<pre><code><b>pragma</b> opaque;
+</code></pre>
+
+
+
+<a id="@Specification_1_dispatchable_derived_supply"></a>
+
+### Function `dispatchable_derived_supply`
+
+
+<pre><code><b>fun</b> <a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset_dispatchable_derived_supply">dispatchable_derived_supply</a>&lt;T: key&gt;(store: <a href="object.md#0x1_object_Object">object::Object</a>&lt;T&gt;, function: &<a href="function_info.md#0x1_function_info_FunctionInfo">function_info::FunctionInfo</a>): <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_Option">option::Option</a>&lt;u128&gt;
+</code></pre>
+
+
+
+
 <pre><code><b>pragma</b> opaque;
 </code></pre>
 
diff --git a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/fungible_asset.md b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/fungible_asset.md
index 3f215d00bed96..0cac9507ce215 100644
--- a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/fungible_asset.md
+++ b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/fungible_asset.md
@@ -13,6 +13,7 @@ metadata object can be any object that equipped with <code><a href="fungible_ass
 -  [Resource `Untransferable`](#0x1_fungible_asset_Untransferable)
 -  [Resource `FungibleStore`](#0x1_fungible_asset_FungibleStore)
 -  [Resource `DispatchFunctionStore`](#0x1_fungible_asset_DispatchFunctionStore)
+-  [Resource `DeriveSupply`](#0x1_fungible_asset_DeriveSupply)
 -  [Resource `ConcurrentFungibleBalance`](#0x1_fungible_asset_ConcurrentFungibleBalance)
 -  [Struct `FungibleAsset`](#0x1_fungible_asset_FungibleAsset)
 -  [Struct `MintRef`](#0x1_fungible_asset_MintRef)
@@ -34,6 +35,8 @@ metadata object can be any object that equipped with <code><a href="fungible_ass
 -  [Function `set_untransferable`](#0x1_fungible_asset_set_untransferable)
 -  [Function `is_untransferable`](#0x1_fungible_asset_is_untransferable)
 -  [Function `register_dispatch_functions`](#0x1_fungible_asset_register_dispatch_functions)
+-  [Function `register_derive_supply_dispatch_function`](#0x1_fungible_asset_register_derive_supply_dispatch_function)
+-  [Function `register_dispatch_function_sanity_check`](#0x1_fungible_asset_register_dispatch_function_sanity_check)
 -  [Function `generate_mint_ref`](#0x1_fungible_asset_generate_mint_ref)
 -  [Function `generate_burn_ref`](#0x1_fungible_asset_generate_burn_ref)
 -  [Function `generate_transfer_ref`](#0x1_fungible_asset_generate_transfer_ref)
@@ -62,6 +65,7 @@ metadata object can be any object that equipped with <code><a href="fungible_ass
 -  [Function `withdraw_dispatch_function`](#0x1_fungible_asset_withdraw_dispatch_function)
 -  [Function `has_withdraw_dispatch_function`](#0x1_fungible_asset_has_withdraw_dispatch_function)
 -  [Function `derived_balance_dispatch_function`](#0x1_fungible_asset_derived_balance_dispatch_function)
+-  [Function `derived_supply_dispatch_function`](#0x1_fungible_asset_derived_supply_dispatch_function)
 -  [Function `asset_metadata`](#0x1_fungible_asset_asset_metadata)
 -  [Function `mint_ref_metadata`](#0x1_fungible_asset_mint_ref_metadata)
 -  [Function `transfer_ref_metadata`](#0x1_fungible_asset_transfer_ref_metadata)
@@ -348,6 +352,34 @@ The store object that holds fungible assets of a specific type associated with a
 </dl>
 
 
+</details>
+
+<a id="0x1_fungible_asset_DeriveSupply"></a>
+
+## Resource `DeriveSupply`
+
+
+
+<pre><code>#[resource_group_member(#[group = <a href="object.md#0x1_object_ObjectGroup">0x1::object::ObjectGroup</a>])]
+<b>struct</b> <a href="fungible_asset.md#0x1_fungible_asset_DeriveSupply">DeriveSupply</a> <b>has</b> key
+</code></pre>
+
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>dispatch_function: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_Option">option::Option</a>&lt;<a href="function_info.md#0x1_function_info_FunctionInfo">function_info::FunctionInfo</a>&gt;</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
 </details>
 
 <a id="0x1_fungible_asset_ConcurrentFungibleBalance"></a>
@@ -892,6 +924,16 @@ Provided derived_balance function type doesn't meet the signature requirement.
 
 
 
+<a id="0x1_fungible_asset_EDERIVED_SUPPLY_FUNCTION_SIGNATURE_MISMATCH"></a>
+
+Provided derived_supply function type doesn't meet the signature requirement.
+
+
+<pre><code><b>const</b> <a href="fungible_asset.md#0x1_fungible_asset_EDERIVED_SUPPLY_FUNCTION_SIGNATURE_MISMATCH">EDERIVED_SUPPLY_FUNCTION_SIGNATURE_MISMATCH</a>: u64 = 33;
+</code></pre>
+
+
+
 <a id="0x1_fungible_asset_EFUNGIBLE_ASSET_AND_STORE_MISMATCH"></a>
 
 Fungible asset and store do not match.
@@ -1403,28 +1445,13 @@ Create a fungible asset store whose transfer rule would be overloaded by the pro
             )
         );
     });
-
-    // Cannot register hook for APT.
-    <b>assert</b>!(
-        <a href="object.md#0x1_object_address_from_constructor_ref">object::address_from_constructor_ref</a>(constructor_ref) != @aptos_fungible_asset,
-        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_permission_denied">error::permission_denied</a>(<a href="fungible_asset.md#0x1_fungible_asset_EAPT_NOT_DISPATCHABLE">EAPT_NOT_DISPATCHABLE</a>)
-    );
-    <b>assert</b>!(
-        !<a href="object.md#0x1_object_can_generate_delete_ref">object::can_generate_delete_ref</a>(constructor_ref),
-        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="fungible_asset.md#0x1_fungible_asset_EOBJECT_IS_DELETABLE">EOBJECT_IS_DELETABLE</a>)
-    );
+    <a href="fungible_asset.md#0x1_fungible_asset_register_dispatch_function_sanity_check">register_dispatch_function_sanity_check</a>(constructor_ref);
     <b>assert</b>!(
         !<b>exists</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_DispatchFunctionStore">DispatchFunctionStore</a>&gt;(
             <a href="object.md#0x1_object_address_from_constructor_ref">object::address_from_constructor_ref</a>(constructor_ref)
         ),
         <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_already_exists">error::already_exists</a>(<a href="fungible_asset.md#0x1_fungible_asset_EALREADY_REGISTERED">EALREADY_REGISTERED</a>)
     );
-    <b>assert</b>!(
-        <b>exists</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_Metadata">Metadata</a>&gt;(
-            <a href="object.md#0x1_object_address_from_constructor_ref">object::address_from_constructor_ref</a>(constructor_ref)
-        ),
-        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_not_found">error::not_found</a>(<a href="fungible_asset.md#0x1_fungible_asset_EFUNGIBLE_METADATA_EXISTENCE">EFUNGIBLE_METADATA_EXISTENCE</a>),
-    );
 
     <b>let</b> store_obj = &<a href="object.md#0x1_object_generate_signer">object::generate_signer</a>(constructor_ref);
 
@@ -1442,6 +1469,110 @@ Create a fungible asset store whose transfer rule would be overloaded by the pro
 
 
 
+</details>
+
+<a id="0x1_fungible_asset_register_derive_supply_dispatch_function"></a>
+
+## Function `register_derive_supply_dispatch_function`
+
+Define the derived supply dispatch with the provided function.
+
+
+<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_register_derive_supply_dispatch_function">register_derive_supply_dispatch_function</a>(constructor_ref: &<a href="object.md#0x1_object_ConstructorRef">object::ConstructorRef</a>, dispatch_function: <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_Option">option::Option</a>&lt;<a href="function_info.md#0x1_function_info_FunctionInfo">function_info::FunctionInfo</a>&gt;)
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_register_derive_supply_dispatch_function">register_derive_supply_dispatch_function</a>(
+    constructor_ref: &ConstructorRef,
+    dispatch_function: Option&lt;FunctionInfo&gt;
+) {
+    // Verify that caller type matches callee type so wrongly typed function cannot be registered.
+    <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_for_each_ref">option::for_each_ref</a>(&dispatch_function, |supply_function| {
+        <b>let</b> <a href="function_info.md#0x1_function_info">function_info</a> = <a href="function_info.md#0x1_function_info_new_function_info_from_address">function_info::new_function_info_from_address</a>(
+            @aptos_framework,
+            <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/string.md#0x1_string_utf8">string::utf8</a>(b"<a href="dispatchable_fungible_asset.md#0x1_dispatchable_fungible_asset">dispatchable_fungible_asset</a>"),
+            <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/string.md#0x1_string_utf8">string::utf8</a>(b"dispatchable_derived_supply"),
+        );
+        // Verify that caller type matches callee type so wrongly typed function cannot be registered.
+        <b>assert</b>!(
+            <a href="function_info.md#0x1_function_info_check_dispatch_type_compatibility">function_info::check_dispatch_type_compatibility</a>(
+                &<a href="function_info.md#0x1_function_info">function_info</a>,
+                supply_function
+            ),
+            <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(
+                <a href="fungible_asset.md#0x1_fungible_asset_EDERIVED_SUPPLY_FUNCTION_SIGNATURE_MISMATCH">EDERIVED_SUPPLY_FUNCTION_SIGNATURE_MISMATCH</a>
+            )
+        );
+    });
+    <a href="fungible_asset.md#0x1_fungible_asset_register_dispatch_function_sanity_check">register_dispatch_function_sanity_check</a>(constructor_ref);
+    <b>assert</b>!(
+        !<b>exists</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_DeriveSupply">DeriveSupply</a>&gt;(
+            <a href="object.md#0x1_object_address_from_constructor_ref">object::address_from_constructor_ref</a>(constructor_ref)
+        ),
+        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_already_exists">error::already_exists</a>(<a href="fungible_asset.md#0x1_fungible_asset_EALREADY_REGISTERED">EALREADY_REGISTERED</a>)
+    );
+
+
+    <b>let</b> store_obj = &<a href="object.md#0x1_object_generate_signer">object::generate_signer</a>(constructor_ref);
+
+    // Store the overload function hook.
+    <b>move_to</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_DeriveSupply">DeriveSupply</a>&gt;(
+        store_obj,
+        <a href="fungible_asset.md#0x1_fungible_asset_DeriveSupply">DeriveSupply</a> {
+            dispatch_function
+        }
+    );
+}
+</code></pre>
+
+
+
+</details>
+
+<a id="0x1_fungible_asset_register_dispatch_function_sanity_check"></a>
+
+## Function `register_dispatch_function_sanity_check`
+
+Check the requirements for registering a dispatchable function.
+
+
+<pre><code><b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_register_dispatch_function_sanity_check">register_dispatch_function_sanity_check</a>(constructor_ref: &<a href="object.md#0x1_object_ConstructorRef">object::ConstructorRef</a>)
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code>inline <b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_register_dispatch_function_sanity_check">register_dispatch_function_sanity_check</a>(
+    constructor_ref: &ConstructorRef,
+)  {
+    // Cannot register hook for APT.
+    <b>assert</b>!(
+        <a href="object.md#0x1_object_address_from_constructor_ref">object::address_from_constructor_ref</a>(constructor_ref) != @aptos_fungible_asset,
+        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_permission_denied">error::permission_denied</a>(<a href="fungible_asset.md#0x1_fungible_asset_EAPT_NOT_DISPATCHABLE">EAPT_NOT_DISPATCHABLE</a>)
+    );
+    <b>assert</b>!(
+        !<a href="object.md#0x1_object_can_generate_delete_ref">object::can_generate_delete_ref</a>(constructor_ref),
+        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="fungible_asset.md#0x1_fungible_asset_EOBJECT_IS_DELETABLE">EOBJECT_IS_DELETABLE</a>)
+    );
+    <b>assert</b>!(
+        <b>exists</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_Metadata">Metadata</a>&gt;(
+            <a href="object.md#0x1_object_address_from_constructor_ref">object::address_from_constructor_ref</a>(constructor_ref)
+        ),
+        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_not_found">error::not_found</a>(<a href="fungible_asset.md#0x1_fungible_asset_EFUNGIBLE_METADATA_EXISTENCE">EFUNGIBLE_METADATA_EXISTENCE</a>),
+    );
+}
+</code></pre>
+
+
+
 </details>
 
 <a id="0x1_fungible_asset_generate_mint_ref"></a>
@@ -2243,6 +2374,35 @@ Return whether a fungible asset type is dispatchable.
 
 
 
+</details>
+
+<a id="0x1_fungible_asset_derived_supply_dispatch_function"></a>
+
+## Function `derived_supply_dispatch_function`
+
+
+
+<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_derived_supply_dispatch_function">derived_supply_dispatch_function</a>&lt;T: key&gt;(metadata: <a href="object.md#0x1_object_Object">object::Object</a>&lt;T&gt;): <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_Option">option::Option</a>&lt;<a href="function_info.md#0x1_function_info_FunctionInfo">function_info::FunctionInfo</a>&gt;
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_derived_supply_dispatch_function">derived_supply_dispatch_function</a>&lt;T: key&gt;(metadata: Object&lt;T&gt;): Option&lt;FunctionInfo&gt; <b>acquires</b> <a href="fungible_asset.md#0x1_fungible_asset_DeriveSupply">DeriveSupply</a> {
+    <b>let</b> metadata_addr = <a href="object.md#0x1_object_object_address">object::object_address</a>(&metadata);
+    <b>if</b> (<b>exists</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_DeriveSupply">DeriveSupply</a>&gt;(metadata_addr)) {
+        <b>borrow_global</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_DeriveSupply">DeriveSupply</a>&gt;(metadata_addr).dispatch_function
+    } <b>else</b> {
+        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_none">option::none</a>()
+    }
+}
+</code></pre>
+
+
+
 </details>
 
 <a id="0x1_fungible_asset_asset_metadata"></a>
@@ -3161,12 +3321,12 @@ Destroy an empty fungible asset.
 
 <pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_deposit_internal">deposit_internal</a>(store_addr: <b>address</b>, fa: <a href="fungible_asset.md#0x1_fungible_asset_FungibleAsset">FungibleAsset</a>) <b>acquires</b> <a href="fungible_asset.md#0x1_fungible_asset_FungibleStore">FungibleStore</a>, <a href="fungible_asset.md#0x1_fungible_asset_ConcurrentFungibleBalance">ConcurrentFungibleBalance</a> {
     <b>let</b> <a href="fungible_asset.md#0x1_fungible_asset_FungibleAsset">FungibleAsset</a> { metadata, amount } = fa;
-    <b>if</b> (amount == 0) <b>return</b>;
-
     <b>assert</b>!(<b>exists</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_FungibleStore">FungibleStore</a>&gt;(store_addr), <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_not_found">error::not_found</a>(<a href="fungible_asset.md#0x1_fungible_asset_EFUNGIBLE_STORE_EXISTENCE">EFUNGIBLE_STORE_EXISTENCE</a>));
     <b>let</b> store = <b>borrow_global_mut</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_FungibleStore">FungibleStore</a>&gt;(store_addr);
     <b>assert</b>!(metadata == store.metadata, <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="fungible_asset.md#0x1_fungible_asset_EFUNGIBLE_ASSET_AND_STORE_MISMATCH">EFUNGIBLE_ASSET_AND_STORE_MISMATCH</a>));
 
+    <b>if</b> (amount == 0) <b>return</b>;
+
     <b>if</b> (store.balance == 0 && <a href="fungible_asset.md#0x1_fungible_asset_concurrent_fungible_balance_exists_inline">concurrent_fungible_balance_exists_inline</a>(store_addr)) {
         <b>let</b> balance_resource = <b>borrow_global_mut</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_ConcurrentFungibleBalance">ConcurrentFungibleBalance</a>&gt;(store_addr);
         <a href="aggregator_v2.md#0x1_aggregator_v2_add">aggregator_v2::add</a>(&<b>mut</b> balance_resource.balance, amount);
diff --git a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/randomness.md b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/randomness.md
index 692e0ed3a10b5..80f27e49459c6 100644
--- a/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/randomness.md
+++ b/aptos-move/framework/aptos-framework/tests/compiler-v2-doc/randomness.md
@@ -36,6 +36,7 @@ Security holds under the same proof-of-stake assumption that secures the Aptos n
 -  [Function `u256_range`](#0x1_randomness_u256_range)
 -  [Function `permutation`](#0x1_randomness_permutation)
 -  [Function `safe_add_mod`](#0x1_randomness_safe_add_mod)
+-  [Function `take_first`](#0x1_randomness_take_first)
 -  [Function `fetch_and_increment_txn_counter`](#0x1_randomness_fetch_and_increment_txn_counter)
 -  [Function `is_unbiasable`](#0x1_randomness_is_unbiasable)
 -  [Specification](#@Specification_1)
@@ -318,7 +319,7 @@ Generates a sequence of bytes uniformly at random
     <b>let</b> c = 0;
     <b>while</b> (c &lt; n) {
         <b>let</b> blob = <a href="randomness.md#0x1_randomness_next_32_bytes">next_32_bytes</a>();
-        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector_append">vector::append</a>(&<b>mut</b> v, blob);
+        <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector_reverse_append">vector::reverse_append</a>(&<b>mut</b> v, blob);
 
         c = c + 32;
     };
@@ -825,6 +826,8 @@ If n is 0, returns the empty vector.
 
 
 <pre><code><b>public</b> <b>fun</b> <a href="randomness.md#0x1_randomness_permutation">permutation</a>(n: u64): <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector">vector</a>&lt;u64&gt; <b>acquires</b> <a href="randomness.md#0x1_randomness_PerBlockRandomness">PerBlockRandomness</a> {
+    <a href="event.md#0x1_event_emit">event::emit</a>(<a href="randomness.md#0x1_randomness_RandomnessGeneratedEvent">RandomnessGeneratedEvent</a> {});
+
     <b>let</b> values = <a href="../../../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector">vector</a>[];
 
     <b>if</b>(n == 0) {
@@ -863,8 +866,6 @@ If n is 0, returns the empty vector.
         tail = tail - 1;
     };
 
-    <a href="event.md#0x1_event_emit">event::emit</a>(<a href="randomness.md#0x1_randomness_RandomnessGeneratedEvent">RandomnessGeneratedEvent</a> {});
-
     values
 }
 </code></pre>
@@ -889,18 +890,38 @@ Compute <code>(a + b) % m</code>, assuming <code>m &gt;= 1, 0 &lt;= a &lt; m, 0&
 <summary>Implementation</summary>
 
 
-<pre><code>inline <b>fun</b> <a href="randomness.md#0x1_randomness_safe_add_mod">safe_add_mod</a>(a: u256, b: u256, m: u256): u256 {
+<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_safe_add_mod">safe_add_mod</a>(a: u256, b: u256, m: u256): u256 {
+    <b>let</b> a_clone = a;
     <b>let</b> neg_b = m - b;
-    <b>if</b> (a &lt; neg_b) {
-        a + b
-    } <b>else</b> {
-        a - neg_b
-    }
+    <b>let</b> a_less = a &lt; neg_b;
+    <a href="randomness.md#0x1_randomness_take_first">take_first</a>(<b>if</b> (a_less) { a + b } <b>else</b> { a_clone - neg_b }, <b>if</b> (!a_less) { a_clone - neg_b } <b>else</b> { a + b })
 }
 </code></pre>
 
 
 
+</details>
+
+<a id="0x1_randomness_take_first"></a>
+
+## Function `take_first`
+
+
+
+<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_take_first">take_first</a>(x: u256, _y: u256): u256
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="randomness.md#0x1_randomness_take_first">take_first</a>(x: u256, _y: u256 ): u256 { x }
+</code></pre>
+
+
+
 </details>
 
 <a id="0x1_randomness_fetch_and_increment_txn_counter"></a>
diff --git a/aptos-move/framework/aptos-stdlib/tests/compiler-v2-doc/type_info.md b/aptos-move/framework/aptos-stdlib/tests/compiler-v2-doc/type_info.md
index d482395948234..8cc7cf089708f 100644
--- a/aptos-move/framework/aptos-stdlib/tests/compiler-v2-doc/type_info.md
+++ b/aptos-move/framework/aptos-stdlib/tests/compiler-v2-doc/type_info.md
@@ -280,8 +280,7 @@ analysis of vector size dynamism.
 
 
 <pre><code><b>public</b> <b>fun</b> <a href="type_info.md#0x1_type_info_size_of_val">size_of_val</a>&lt;T&gt;(val_ref: &T): u64 {
-    // Return <a href="../../../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector">vector</a> length of vectorized BCS representation.
-    <a href="../../../move-stdlib/tests/compiler-v2-doc/vector.md#0x1_vector_length">vector::length</a>(&<a href="../../../move-stdlib/tests/compiler-v2-doc/bcs.md#0x1_bcs_to_bytes">bcs::to_bytes</a>(val_ref))
+    <a href="../../../move-stdlib/tests/compiler-v2-doc/bcs.md#0x1_bcs_serialized_size">bcs::serialized_size</a>(val_ref)
 }
 </code></pre>
 
@@ -391,8 +390,7 @@ analysis of vector size dynamism.
 
 
 
-<pre><code><b>aborts_if</b> <b>false</b>;
-<b>ensures</b> result == <a href="type_info.md#0x1_type_info_spec_size_of_val">spec_size_of_val</a>&lt;T&gt;(val_ref);
+<pre><code><b>ensures</b> result == <a href="type_info.md#0x1_type_info_spec_size_of_val">spec_size_of_val</a>&lt;T&gt;(val_ref);
 </code></pre>
 
 
diff --git a/aptos-move/framework/aptos-token-objects/tests/compiler-v2-doc/collection.md b/aptos-move/framework/aptos-token-objects/tests/compiler-v2-doc/collection.md
index d482ee43a4737..1f9f1547c5729 100644
--- a/aptos-move/framework/aptos-token-objects/tests/compiler-v2-doc/collection.md
+++ b/aptos-move/framework/aptos-token-objects/tests/compiler-v2-doc/collection.md
@@ -980,9 +980,6 @@ TODO: Hide this until we bring back meaningful way to enforce burns
         <a href="royalty.md#0x4_royalty_init">royalty::init</a>(&constructor_ref, <a href="../../../aptos-framework/../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_extract">option::extract</a>(&<b>mut</b> <a href="royalty.md#0x4_royalty">royalty</a>))
     };
 
-    <b>let</b> transfer_ref = <a href="../../../aptos-framework/tests/compiler-v2-doc/object.md#0x1_object_generate_transfer_ref">object::generate_transfer_ref</a>(&constructor_ref);
-    <a href="../../../aptos-framework/tests/compiler-v2-doc/object.md#0x1_object_disable_ungated_transfer">object::disable_ungated_transfer</a>(&transfer_ref);
-
     constructor_ref
 }
 </code></pre>
diff --git a/aptos-move/framework/aptos-token-objects/tests/compiler-v2-doc/token.md b/aptos-move/framework/aptos-token-objects/tests/compiler-v2-doc/token.md
index 8205d3e901d59..d5dac5e4158ff 100644
--- a/aptos-move/framework/aptos-token-objects/tests/compiler-v2-doc/token.md
+++ b/aptos-move/framework/aptos-token-objects/tests/compiler-v2-doc/token.md
@@ -380,6 +380,16 @@ The URI is over the maximum length
 
 
 
+<a id="0x4_token_ENOT_OWNER"></a>
+
+The calling signer is not the owner
+
+
+<pre><code><b>const</b> <a href="token.md#0x4_token_ENOT_OWNER">ENOT_OWNER</a>: u64 = 8;
+</code></pre>
+
+
+
 <a id="0x4_token_EDESCRIPTION_TOO_LONG"></a>
 
 The description is over the maximum length
@@ -542,7 +552,7 @@ The token name is over the maximum length
     <a href="royalty.md#0x4_royalty">royalty</a>: Option&lt;Royalty&gt;,
     uri: String,
 ) {
-    <b>assert</b>!(<a href="collection.md#0x4_collection_creator">collection::creator</a>(<a href="collection.md#0x4_collection">collection</a>) == <a href="../../../aptos-framework/../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/signer.md#0x1_signer_address_of">signer::address_of</a>(creator), <a href="../../../aptos-framework/../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_unauthenticated">error::unauthenticated</a>(<a href="token.md#0x4_token_ENOT_CREATOR">ENOT_CREATOR</a>));
+    <b>assert</b>!(<a href="../../../aptos-framework/tests/compiler-v2-doc/object.md#0x1_object_owner">object::owner</a>(<a href="collection.md#0x4_collection">collection</a>) == <a href="../../../aptos-framework/../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/signer.md#0x1_signer_address_of">signer::address_of</a>(creator), <a href="../../../aptos-framework/../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/error.md#0x1_error_unauthenticated">error::unauthenticated</a>(<a href="token.md#0x4_token_ENOT_OWNER">ENOT_OWNER</a>));
 
     <b>if</b> (<a href="../../../aptos-framework/../aptos-stdlib/../move-stdlib/tests/compiler-v2-doc/option.md#0x1_option_is_some">option::is_some</a>(&name_with_index_suffix)) {
         // Be conservative, <b>as</b> we don't know what length the index will be, and <b>assume</b> worst case (20 chars in MAX_U64)
diff --git a/aptos-move/framework/move-stdlib/tests/compiler-v2-doc/bcs.md b/aptos-move/framework/move-stdlib/tests/compiler-v2-doc/bcs.md
index e01e1d89e1a28..9bdcf7f45f7d3 100644
--- a/aptos-move/framework/move-stdlib/tests/compiler-v2-doc/bcs.md
+++ b/aptos-move/framework/move-stdlib/tests/compiler-v2-doc/bcs.md
@@ -10,7 +10,9 @@ details on BCS.
 
 
 -  [Function `to_bytes`](#0x1_bcs_to_bytes)
+-  [Function `serialized_size`](#0x1_bcs_serialized_size)
 -  [Specification](#@Specification_0)
+    -  [Function `serialized_size`](#@Specification_0_serialized_size)
 
 
 <pre><code></code></pre>
@@ -21,7 +23,8 @@ details on BCS.
 
 ## Function `to_bytes`
 
-Return the binary representation of <code>v</code> in BCS (Binary Canonical Serialization) format
+Returns the binary representation of <code>v</code> in BCS (Binary Canonical Serialization) format.
+Aborts with <code>0x1c5</code> error code if serialization fails.
 
 
 <pre><code><b>public</b> <b>fun</b> <a href="bcs.md#0x1_bcs_to_bytes">to_bytes</a>&lt;MoveValue&gt;(v: &MoveValue): <a href="vector.md#0x1_vector">vector</a>&lt;u8&gt;
@@ -38,6 +41,30 @@ Return the binary representation of <code>v</code> in BCS (Binary Canonical Seri
 
 
 
+</details>
+
+<a id="0x1_bcs_serialized_size"></a>
+
+## Function `serialized_size`
+
+Returns the size of the binary representation of <code>v</code> in BCS (Binary Canonical Serialization) format.
+Aborts with <code>0x1c5</code> error code if there is a failure when calculating serialized size.
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="bcs.md#0x1_bcs_serialized_size">serialized_size</a>&lt;MoveValue&gt;(v: &MoveValue): u64
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>native</b> <b>public</b> <b>fun</b> <a href="bcs.md#0x1_bcs_serialized_size">serialized_size</a>&lt;MoveValue&gt;(v: &MoveValue): u64;
+</code></pre>
+
+
+
 </details>
 
 <a id="@Specification_0"></a>
@@ -56,4 +83,21 @@ Native function which is defined in the prover's prelude.
 </code></pre>
 
 
+
+<a id="@Specification_0_serialized_size"></a>
+
+### Function `serialized_size`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="bcs.md#0x1_bcs_serialized_size">serialized_size</a>&lt;MoveValue&gt;(v: &MoveValue): u64
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> opaque;
+<b>ensures</b> result == len(<a href="bcs.md#0x1_bcs_serialize">serialize</a>(v));
+</code></pre>
+
+
 [move-book]: https://aptos.dev/move/book/SUMMARY
diff --git a/third_party/move/move-prover/tests/sources/functional/type_reflection.move b/third_party/move/move-prover/tests/sources/functional/type_reflection.move
index 2e0ba200d3660..0149dd4cc572a 100644
--- a/third_party/move/move-prover/tests/sources/functional/type_reflection.move
+++ b/third_party/move/move-prover/tests/sources/functional/type_reflection.move
@@ -105,6 +105,17 @@ module 0x42::test {
     spec test_type_info_aborts_if_full {
         aborts_if !type_info::spec_is_struct<T>();
     }
+
+    fun generic_type_info_verification_target<A>(): type_info::TypeInfo {
+       type_info::type_of<A>()
+    }
+    spec generic_type_info_verification_target {
+        ensures result == generic_type_info_spec_fun<A>();
+    }
+
+    spec fun generic_type_info_spec_fun<A>(): type_info::TypeInfo {
+        type_info::type_of<A>()
+    }
 }
 
 module 0x43::test {