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

Issue:
[Feature Request][docgen] Support enum in docgen
# 🚀 Feature Request

<!-- A clear and concise description of the feature you are requesting -->

Add support of enum to docgen


Discussion / hints:

Fix patch:
diff --git a/third_party/move/move-prover/move-docgen/src/docgen.rs b/third_party/move/move-prover/move-docgen/src/docgen.rs
index 23556906dab25..7958a0d53e181 100644
--- a/third_party/move/move-prover/move-docgen/src/docgen.rs
+++ b/third_party/move/move-prover/move-docgen/src/docgen.rs
@@ -1173,19 +1173,25 @@ impl<'env> Docgen<'env> {
     fn gen_struct(&self, spec_block_map: &SpecBlockMap<'_>, struct_env: &StructEnv<'_>) {
         let name = struct_env.get_name();
         self.section_header(
-            &self.struct_title(struct_env),
+            &self.struct_or_enum_title(struct_env),
             &self.label_for_module_item(&struct_env.module_env, name),
         );
         self.increment_section_nest();
         self.doc_text(struct_env.get_doc());
-        self.code_block(&self.struct_header_display(struct_env));
+        self.code_block(&self.struct_or_enum_header_display(struct_env));
 
         if self.options.include_impl || (self.options.include_specs && self.options.specs_inlined) {
             // Include field documentation if either impls or specs are present and inlined,
             // because they are used by both.
-            self.begin_collapsed("Fields");
-            self.gen_struct_fields(struct_env);
-            self.end_collapsed();
+            if struct_env.has_variants() {
+                self.begin_collapsed("Variants");
+                self.gen_enum_inner(struct_env);
+                self.end_collapsed();
+            } else {
+                self.begin_collapsed("Fields");
+                self.gen_struct_fields(struct_env);
+                self.end_collapsed();
+            }
         }
 
         if self.options.specs_inlined {
@@ -1199,19 +1205,26 @@ impl<'env> Docgen<'env> {
         self.decrement_section_nest();
     }
 
-    /// Returns "Struct `N`" or "Resource `N`".
-    fn struct_title(&self, struct_env: &StructEnv<'_>) -> String {
+    /// Returns "Struct `N`" or "Resource `N`" or "Enum `N`".
+    fn struct_or_enum_title(&self, struct_env: &StructEnv<'_>) -> String {
         // NOTE(mengxu): although we no longer declare structs with the `resource` keyword, it
         // might be helpful in keeping `Resource N` in struct title as the boogie translator still
         // depends on the `is_resource()` predicate to add additional functions to structs declared
         // with the `key` ability.
-        format!(
-            "{} `{}`",
+        let resource_or_enum = if struct_env.has_variants() {
             if struct_env.has_memory() {
-                "Resource"
+                "Enum Resource"
             } else {
-                "Struct"
-            },
+                "Enum"
+            }
+        } else if struct_env.has_memory() {
+            "Resource"
+        } else {
+            "Struct"
+        };
+        format!(
+            "{} `{}`",
+            resource_or_enum,
             self.name_string(struct_env.get_name())
         )
     }
@@ -1229,8 +1242,8 @@ impl<'env> Docgen<'env> {
         )
     }
 
-    /// Generates code signature for a struct.
-    fn struct_header_display(&self, struct_env: &StructEnv<'_>) -> String {
+    /// Generates code signature for a struct or enum.
+    fn struct_or_enum_header_display(&self, struct_env: &StructEnv<'_>) -> String {
         let name = self.name_string(struct_env.get_name());
         let type_params = self.type_parameter_list_display(struct_env.get_type_parameters());
         let ability_tokens = self.ability_tokens(struct_env.get_abilities());
@@ -1239,12 +1252,21 @@ impl<'env> Docgen<'env> {
             .iter()
             .map(|attr| format!("{}\n", attr))
             .join("");
+        let enum_or_struct = if struct_env.has_variants() {
+            "enum"
+        } else {
+            "struct"
+        };
         if ability_tokens.is_empty() {
-            format!("{}struct {}{}", attributes_string, name, type_params)
+            format!(
+                "{}{} {}{}",
+                attributes_string, enum_or_struct, name, type_params
+            )
         } else {
             format!(
-                "{}struct {}{} has {}",
+                "{}{} {}{} has {}",
                 attributes_string,
+                enum_or_struct,
                 name,
                 type_params,
                 ability_tokens.join(", ")
@@ -1252,6 +1274,7 @@ impl<'env> Docgen<'env> {
         }
     }
 
+    /// Generates doc for struct fields.
     fn gen_struct_fields(&self, struct_env: &StructEnv<'_>) {
         let tctx = self.type_display_context_for_struct(struct_env);
         self.begin_definitions();
@@ -1268,6 +1291,40 @@ impl<'env> Docgen<'env> {
         self.end_definitions();
     }
 
+    /// Generates doc for `variant` of an enum.
+    fn gen_fields_for_variant(&self, struct_env: &StructEnv<'_>, variant: Symbol) {
+        let tctx = self.type_display_context_for_struct(struct_env);
+        self.begin_definitions();
+        for field in struct_env.get_fields_of_variant(variant) {
+            self.definition_text(
+                &format!(
+                    "`{}: {}`",
+                    self.name_string(field.get_name()),
+                    field.get_type().display(&tctx)
+                ),
+                field.get_doc(),
+            );
+        }
+        self.end_definitions();
+    }
+
+    /// Generates doc for fields from all variants of an enum
+    fn gen_enum_fields(&self, struct_env: &StructEnv<'_>) {
+        self.begin_definitions();
+        self.gen_enum_inner(struct_env);
+        self.end_definitions();
+    }
+
+    fn gen_enum_inner(&self, struct_env: &StructEnv<'_>) {
+        for variant in struct_env.get_variants() {
+            self.begin_collapsed(&format!("{}", variant.display(struct_env.symbol_pool())));
+            self.begin_collapsed("Fields");
+            self.gen_fields_for_variant(struct_env, variant);
+            self.end_collapsed();
+            self.end_collapsed();
+        }
+    }
+
     /// Generates documentation for a function.
     fn gen_function(&self, spec_block_map: &SpecBlockMap<'_>, func_env: &FunctionEnv<'_>) {
         let is_script = func_env.module_env.is_script_module();
@@ -1577,11 +1634,15 @@ impl<'env> Docgen<'env> {
             if spec_block_map.contains_key(&target) {
                 let name = self.name_string(struct_env.get_name());
                 self.section_header(
-                    &self.struct_title(&struct_env),
+                    &self.struct_or_enum_title(&struct_env),
                     &format!("{}_{}", section_label, name),
                 );
-                self.code_block(&self.struct_header_display(&struct_env));
-                self.gen_struct_fields(&struct_env);
+                self.code_block(&self.struct_or_enum_header_display(&struct_env));
+                if struct_env.has_variants() {
+                    self.gen_enum_fields(&struct_env);
+                } else {
+                    self.gen_struct_fields(&struct_env);
+                }
                 self.gen_spec_blocks(module_env, "", &target, spec_block_map);
             }
         }


Test patch:
diff --git a/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.move b/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.move
new file mode 100644
index 0000000000000..a77329ed5ce8f
--- /dev/null
+++ b/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.move
@@ -0,0 +1,86 @@
+module 0x815::m {
+
+    enum CommonFields has key, copy, drop {
+        Foo{x: u64, y: u8},
+        Bar{x: u64, y: u8, z: u32}
+    }
+
+    spec CommonFields {
+        invariant self.x > 20;
+        invariant (self is CommonFields::Bar) ==> self.z > 10;
+    }
+
+    fun t9_common_field(): u64 {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        common.x = 15; // struct invariant fails
+        common.x
+    }
+
+    fun test_data_invariant() {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let CommonFields::Bar {x: _x, y: _y, z} = &mut common;
+        *z = 9; // struct invariant fails
+    }
+
+    fun test_match_ref(): u64 {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        match (&common) {
+            Foo {x, y: _} => *x,
+            Bar {x, y: _, z: _ } => *x + 1
+        }
+    }
+
+    spec test_match_ref {
+        ensures result == 31;
+    }
+
+    enum CommonFieldsVector has drop {
+        Foo{x: vector<u8>},
+        Bar{x: vector<u8>, y: vector<CommonFields>}
+    }
+
+    fun test_enum_vector() {
+        let _common_vector_1 = CommonFieldsVector::Foo {
+            x: vector[2]
+        };
+        let _common_fields = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let _common_vector_2 = CommonFieldsVector::Bar {
+            x: vector[2],
+            y: vector[_common_fields]
+        };
+        spec {
+            assert _common_vector_1.x != _common_vector_2.x; // this fails
+            assert _common_vector_2.y[0] == CommonFields::Bar {
+                x: 30,
+                y: 40,
+                z: 50
+            };
+        };
+        let _common_vector_3 = CommonFieldsVector::Bar {
+            x: vector[2],
+            y: vector[_common_fields]
+        };
+        spec {
+            assert _common_vector_2.x == _common_vector_3.x;
+            assert _common_vector_2 == _common_vector_3;
+        };
+
+    }
+
+}
diff --git a/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_inline.md b/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_inline.md
new file mode 100644
index 0000000000000..232782ad32505
--- /dev/null
+++ b/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_inline.md
@@ -0,0 +1,333 @@
+
+<a id="0x815_m"></a>
+
+# Module `0x815::m`
+
+
+
+-  [Enum Resource `CommonFields`](#0x815_m_CommonFields)
+-  [Enum `CommonFieldsVector`](#0x815_m_CommonFieldsVector)
+-  [Function `t9_common_field`](#0x815_m_t9_common_field)
+-  [Function `test_data_invariant`](#0x815_m_test_data_invariant)
+-  [Function `test_match_ref`](#0x815_m_test_match_ref)
+-  [Function `test_enum_vector`](#0x815_m_test_enum_vector)
+
+
+<pre><code></code></pre>
+
+
+
+<a id="0x815_m_CommonFields"></a>
+
+## Enum Resource `CommonFields`
+
+
+
+<pre><code>enum <a href="enum.md#0x815_m_CommonFields">CommonFields</a> <b>has</b> <b>copy</b>, drop, key
+</code></pre>
+
+
+
+<details>
+<summary>Variants</summary>
+
+
+<details>
+<summary>Foo</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: u64</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: u8</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+<details>
+<summary>Bar</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: u64</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: u8</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>z: u32</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+</details>
+
+<details>
+<summary>Specification</summary>
+
+
+
+<pre><code><b>invariant</b> self.x &gt; 20;
+<b>invariant</b> (self is CommonFields::Bar) ==&gt; self.z &gt; 10;
+</code></pre>
+
+
+
+</details>
+
+<a id="0x815_m_CommonFieldsVector"></a>
+
+## Enum `CommonFieldsVector`
+
+
+
+<pre><code>enum <a href="enum.md#0x815_m_CommonFieldsVector">CommonFieldsVector</a> <b>has</b> drop
+</code></pre>
+
+
+
+<details>
+<summary>Variants</summary>
+
+
+<details>
+<summary>Foo</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: <a href="">vector</a>&lt;u8&gt;</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+<details>
+<summary>Bar</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: <a href="">vector</a>&lt;u8&gt;</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: <a href="">vector</a>&lt;<a href="enum.md#0x815_m_CommonFields">m::CommonFields</a>&gt;</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+</details>
+
+<a id="0x815_m_t9_common_field"></a>
+
+## Function `t9_common_field`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_t9_common_field">t9_common_field</a>(): u64
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_t9_common_field">t9_common_field</a>(): u64 {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    common.x = 15; // <b>struct</b> <b>invariant</b> fails
+    common.x
+}
+</code></pre>
+
+
+
+</details>
+
+<a id="0x815_m_test_data_invariant"></a>
+
+## Function `test_data_invariant`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_data_invariant">test_data_invariant</a>()
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_data_invariant">test_data_invariant</a>() {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    <b>let</b> CommonFields::Bar {x: _x, y: _y, z} = &<b>mut</b> common;
+    *z = 9; // <b>struct</b> <b>invariant</b> fails
+}
+</code></pre>
+
+
+
+</details>
+
+<a id="0x815_m_test_match_ref"></a>
+
+## Function `test_match_ref`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_match_ref">test_match_ref</a>(): u64
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_match_ref">test_match_ref</a>(): u64 {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    match (&common) {
+        Foo {x, y: _} =&gt; *x,
+        Bar {x, y: _, z: _ } =&gt; *x + 1
+    }
+}
+</code></pre>
+
+
+
+</details>
+
+<details>
+<summary>Specification</summary>
+
+
+
+<pre><code><b>ensures</b> result == 31;
+</code></pre>
+
+
+
+</details>
+
+<a id="0x815_m_test_enum_vector"></a>
+
+## Function `test_enum_vector`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_enum_vector">test_enum_vector</a>()
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_enum_vector">test_enum_vector</a>() {
+    <b>let</b> _common_vector_1 = CommonFieldsVector::Foo {
+        x: <a href="">vector</a>[2]
+    };
+    <b>let</b> _common_fields = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    <b>let</b> _common_vector_2 = CommonFieldsVector::Bar {
+        x: <a href="">vector</a>[2],
+        y: <a href="">vector</a>[_common_fields]
+    };
+    <b>spec</b> {
+        <b>assert</b> _common_vector_1.x != _common_vector_2.x; // this fails
+        <b>assert</b> _common_vector_2.y[0] == CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+    };
+    <b>let</b> _common_vector_3 = CommonFieldsVector::Bar {
+        x: <a href="">vector</a>[2],
+        y: <a href="">vector</a>[_common_fields]
+    };
+    <b>spec</b> {
+        <b>assert</b> _common_vector_2.x == _common_vector_3.x;
+        <b>assert</b> _common_vector_2 == _common_vector_3;
+    };
+
+}
+</code></pre>
+
+
+
+</details>
diff --git a/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_inline_no_fold.md b/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_inline_no_fold.md
new file mode 100644
index 0000000000000..18ea9abc8e088
--- /dev/null
+++ b/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_inline_no_fold.md
@@ -0,0 +1,283 @@
+
+<a id="0x815_m"></a>
+
+# Module `0x815::m`
+
+
+
+-  [Enum Resource `CommonFields`](#0x815_m_CommonFields)
+-  [Enum `CommonFieldsVector`](#0x815_m_CommonFieldsVector)
+-  [Function `t9_common_field`](#0x815_m_t9_common_field)
+-  [Function `test_data_invariant`](#0x815_m_test_data_invariant)
+-  [Function `test_match_ref`](#0x815_m_test_match_ref)
+-  [Function `test_enum_vector`](#0x815_m_test_enum_vector)
+
+
+<pre><code></code></pre>
+
+
+
+<a id="0x815_m_CommonFields"></a>
+
+## Enum Resource `CommonFields`
+
+
+
+<pre><code>enum <a href="enum.md#0x815_m_CommonFields">CommonFields</a> <b>has</b> <b>copy</b>, drop, key
+</code></pre>
+
+
+
+##### Variants
+
+
+##### Foo
+
+
+##### Fields
+
+
+<dl>
+<dt>
+<code>x: u64</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: u8</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+##### Bar
+
+
+##### Fields
+
+
+<dl>
+<dt>
+<code>x: u64</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: u8</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>z: u32</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+##### Specification
+
+
+
+<pre><code><b>invariant</b> self.x &gt; 20;
+<b>invariant</b> (self is CommonFields::Bar) ==&gt; self.z &gt; 10;
+</code></pre>
+
+
+
+<a id="0x815_m_CommonFieldsVector"></a>
+
+## Enum `CommonFieldsVector`
+
+
+
+<pre><code>enum <a href="enum.md#0x815_m_CommonFieldsVector">CommonFieldsVector</a> <b>has</b> drop
+</code></pre>
+
+
+
+##### Variants
+
+
+##### Foo
+
+
+##### Fields
+
+
+<dl>
+<dt>
+<code>x: <a href="">vector</a>&lt;u8&gt;</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+##### Bar
+
+
+##### Fields
+
+
+<dl>
+<dt>
+<code>x: <a href="">vector</a>&lt;u8&gt;</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: <a href="">vector</a>&lt;<a href="enum.md#0x815_m_CommonFields">m::CommonFields</a>&gt;</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+<a id="0x815_m_t9_common_field"></a>
+
+## Function `t9_common_field`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_t9_common_field">t9_common_field</a>(): u64
+</code></pre>
+
+
+
+##### Implementation
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_t9_common_field">t9_common_field</a>(): u64 {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    common.x = 15; // <b>struct</b> <b>invariant</b> fails
+    common.x
+}
+</code></pre>
+
+
+
+<a id="0x815_m_test_data_invariant"></a>
+
+## Function `test_data_invariant`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_data_invariant">test_data_invariant</a>()
+</code></pre>
+
+
+
+##### Implementation
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_data_invariant">test_data_invariant</a>() {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    <b>let</b> CommonFields::Bar {x: _x, y: _y, z} = &<b>mut</b> common;
+    *z = 9; // <b>struct</b> <b>invariant</b> fails
+}
+</code></pre>
+
+
+
+<a id="0x815_m_test_match_ref"></a>
+
+## Function `test_match_ref`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_match_ref">test_match_ref</a>(): u64
+</code></pre>
+
+
+
+##### Implementation
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_match_ref">test_match_ref</a>(): u64 {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    match (&common) {
+        Foo {x, y: _} =&gt; *x,
+        Bar {x, y: _, z: _ } =&gt; *x + 1
+    }
+}
+</code></pre>
+
+
+
+##### Specification
+
+
+
+<pre><code><b>ensures</b> result == 31;
+</code></pre>
+
+
+
+<a id="0x815_m_test_enum_vector"></a>
+
+## Function `test_enum_vector`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_enum_vector">test_enum_vector</a>()
+</code></pre>
+
+
+
+##### Implementation
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_enum_vector">test_enum_vector</a>() {
+    <b>let</b> _common_vector_1 = CommonFieldsVector::Foo {
+        x: <a href="">vector</a>[2]
+    };
+    <b>let</b> _common_fields = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    <b>let</b> _common_vector_2 = CommonFieldsVector::Bar {
+        x: <a href="">vector</a>[2],
+        y: <a href="">vector</a>[_common_fields]
+    };
+    <b>spec</b> {
+        <b>assert</b> _common_vector_1.x != _common_vector_2.x; // this fails
+        <b>assert</b> _common_vector_2.y[0] == CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+    };
+    <b>let</b> _common_vector_3 = CommonFieldsVector::Bar {
+        x: <a href="">vector</a>[2],
+        y: <a href="">vector</a>[_common_fields]
+    };
+    <b>spec</b> {
+        <b>assert</b> _common_vector_2.x == _common_vector_3.x;
+        <b>assert</b> _common_vector_2 == _common_vector_3;
+    };
+
+}
+</code></pre>
diff --git a/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_separate.md b/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_separate.md
new file mode 100644
index 0000000000000..985c740d36623
--- /dev/null
+++ b/third_party/move/move-prover/move-docgen/tests/sources/test-compiler-v2/enum.spec_separate.md
@@ -0,0 +1,413 @@
+
+<a id="0x815_m"></a>
+
+# Module `0x815::m`
+
+
+
+-  [Enum Resource `CommonFields`](#0x815_m_CommonFields)
+-  [Enum `CommonFieldsVector`](#0x815_m_CommonFieldsVector)
+-  [Function `t9_common_field`](#0x815_m_t9_common_field)
+-  [Function `test_data_invariant`](#0x815_m_test_data_invariant)
+-  [Function `test_match_ref`](#0x815_m_test_match_ref)
+-  [Function `test_enum_vector`](#0x815_m_test_enum_vector)
+-  [Specification](#@Specification_0)
+    -  [Enum Resource `CommonFields`](#@Specification_0_CommonFields)
+    -  [Function `test_match_ref`](#@Specification_0_test_match_ref)
+
+
+<pre><code></code></pre>
+
+
+
+<a id="0x815_m_CommonFields"></a>
+
+## Enum Resource `CommonFields`
+
+
+
+<pre><code>enum <a href="enum.md#0x815_m_CommonFields">CommonFields</a> <b>has</b> <b>copy</b>, drop, key
+</code></pre>
+
+
+
+<details>
+<summary>Variants</summary>
+
+
+<details>
+<summary>Foo</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: u64</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: u8</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+<details>
+<summary>Bar</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: u64</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: u8</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>z: u32</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+</details>
+
+<a id="0x815_m_CommonFieldsVector"></a>
+
+## Enum `CommonFieldsVector`
+
+
+
+<pre><code>enum <a href="enum.md#0x815_m_CommonFieldsVector">CommonFieldsVector</a> <b>has</b> drop
+</code></pre>
+
+
+
+<details>
+<summary>Variants</summary>
+
+
+<details>
+<summary>Foo</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: <a href="">vector</a>&lt;u8&gt;</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+<details>
+<summary>Bar</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: <a href="">vector</a>&lt;u8&gt;</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: <a href="">vector</a>&lt;<a href="enum.md#0x815_m_CommonFields">m::CommonFields</a>&gt;</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+</details>
+
+<a id="0x815_m_t9_common_field"></a>
+
+## Function `t9_common_field`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_t9_common_field">t9_common_field</a>(): u64
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_t9_common_field">t9_common_field</a>(): u64 {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    common.x = 15; // <b>struct</b> <b>invariant</b> fails
+    common.x
+}
+</code></pre>
+
+
+
+</details>
+
+<a id="0x815_m_test_data_invariant"></a>
+
+## Function `test_data_invariant`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_data_invariant">test_data_invariant</a>()
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_data_invariant">test_data_invariant</a>() {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    <b>let</b> CommonFields::Bar {x: _x, y: _y, z} = &<b>mut</b> common;
+    *z = 9; // <b>struct</b> <b>invariant</b> fails
+}
+</code></pre>
+
+
+
+</details>
+
+<a id="0x815_m_test_match_ref"></a>
+
+## Function `test_match_ref`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_match_ref">test_match_ref</a>(): u64
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_match_ref">test_match_ref</a>(): u64 {
+    <b>let</b> common = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    match (&common) {
+        Foo {x, y: _} =&gt; *x,
+        Bar {x, y: _, z: _ } =&gt; *x + 1
+    }
+}
+</code></pre>
+
+
+
+</details>
+
+<a id="0x815_m_test_enum_vector"></a>
+
+## Function `test_enum_vector`
+
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_enum_vector">test_enum_vector</a>()
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_enum_vector">test_enum_vector</a>() {
+    <b>let</b> _common_vector_1 = CommonFieldsVector::Foo {
+        x: <a href="">vector</a>[2]
+    };
+    <b>let</b> _common_fields = CommonFields::Bar {
+        x: 30,
+        y: 40,
+        z: 50
+    };
+    <b>let</b> _common_vector_2 = CommonFieldsVector::Bar {
+        x: <a href="">vector</a>[2],
+        y: <a href="">vector</a>[_common_fields]
+    };
+    <b>spec</b> {
+        <b>assert</b> _common_vector_1.x != _common_vector_2.x; // this fails
+        <b>assert</b> _common_vector_2.y[0] == CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+    };
+    <b>let</b> _common_vector_3 = CommonFieldsVector::Bar {
+        x: <a href="">vector</a>[2],
+        y: <a href="">vector</a>[_common_fields]
+    };
+    <b>spec</b> {
+        <b>assert</b> _common_vector_2.x == _common_vector_3.x;
+        <b>assert</b> _common_vector_2 == _common_vector_3;
+    };
+
+}
+</code></pre>
+
+
+
+</details>
+
+<a id="@Specification_0"></a>
+
+## Specification
+
+
+<a id="@Specification_0_CommonFields"></a>
+
+### Enum Resource `CommonFields`
+
+
+<pre><code>enum <a href="enum.md#0x815_m_CommonFields">CommonFields</a> <b>has</b> <b>copy</b>, drop, key
+</code></pre>
+
+
+
+<dl>
+
+<details>
+<summary>Foo</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: u64</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: u8</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+
+<details>
+<summary>Bar</summary>
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>x: u64</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>y: u8</code>
+</dt>
+<dd>
+
+</dd>
+<dt>
+<code>z: u32</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
+</details>
+
+</details>
+</dl>
+
+
+
+<pre><code><b>invariant</b> self.x &gt; 20;
+<b>invariant</b> (self is CommonFields::Bar) ==&gt; self.z &gt; 10;
+</code></pre>
+
+
+
+<a id="@Specification_0_test_match_ref"></a>
+
+### Function `test_match_ref`
+
+
+<pre><code><b>fun</b> <a href="enum.md#0x815_m_test_match_ref">test_match_ref</a>(): u64
+</code></pre>
+
+
+
+
+<pre><code><b>ensures</b> result == 31;
+</code></pre>
diff --git a/third_party/move/move-prover/move-docgen/tests/testsuite.rs b/third_party/move/move-prover/move-docgen/tests/testsuite.rs
index 375db290fc2a2..a0ea0cfa648c2 100644
--- a/third_party/move/move-prover/move-docgen/tests/testsuite.rs
+++ b/third_party/move/move-prover/move-docgen/tests/testsuite.rs
@@ -6,7 +6,8 @@ use codespan_reporting::term::termcolor::Buffer;
 use itertools::Itertools;
 #[allow(unused_imports)]
 use log::debug;
-use move_prover::{cli::Options, run_move_prover};
+use move_model::metadata::LanguageVersion;
+use move_prover::{cli::Options, run_move_prover, run_move_prover_v2};
 use move_prover_test_utils::baseline_test::verify_or_update_baseline;
 use std::{
     fs::File,
@@ -23,6 +24,8 @@ const FLAGS: &[&str] = &[
     "--skip-attribute-checks",
 ];
 
+const V2_TEST_DIR: &str = "test-compiler-v2";
+
 fn test_runner(path: &Path) -> datatest_stable::Result<()> {
     let mut args = vec!["mvp_test".to_string()];
     args.extend(FLAGS.iter().map(|s| (*s).to_string()).collect_vec());
@@ -86,8 +89,18 @@ fn test_docgen(path: &Path, mut options: Options, suffix: &str) -> anyhow::Resul
     );
     temp_path.push(&base_name);
 
+    if path.to_str().is_some_and(|s| s.contains(V2_TEST_DIR)) {
+        options.compiler_v2 = true;
+        options.language_version = Some(LanguageVersion::V2_0);
+    }
+
     let mut error_writer = Buffer::no_color();
-    let mut output = match run_move_prover(&mut error_writer, options) {
+    let prover_runner = if path.to_str().is_some_and(|s| s.contains(V2_TEST_DIR)) {
+        run_move_prover_v2
+    } else {
+        run_move_prover
+    };
+    let mut output = match prover_runner(&mut error_writer, options) {
         Ok(()) => {
             let mut contents = String::new();
             debug!("writing to {}", temp_path.display());