movement-network · ganymedio · May 3, 2026 · May 3, 2026
@@ -38,6 +38,7 @@ members = [
     "aptos-move/e2e-tests",
     "aptos-move/e2e-testsuite",
     "aptos-move/framework",
+    "aptos-move/framework/formal/difftest",
     "aptos-move/framework/cached-packages",
     "aptos-move/framework/table-natives",
     "aptos-move/move-examples",

@@ -68,6 +68,7 @@ metadata object can be any object that equipped with <code><a href="fungible_ass
 -  [Function `is_address_balance_at_least`](#0x1_fungible_asset_is_address_balance_at_least)
 -  [Function `is_frozen`](#0x1_fungible_asset_is_frozen)
 -  [Function `is_store_dispatchable`](#0x1_fungible_asset_is_store_dispatchable)
+-  [Function `is_asset_type_dispatchable`](#0x1_fungible_asset_is_asset_type_dispatchable)
 -  [Function `deposit_dispatch_function`](#0x1_fungible_asset_deposit_dispatch_function)
 -  [Function `has_deposit_dispatch_function`](#0x1_fungible_asset_has_deposit_dispatch_function)
 -  [Function `withdraw_dispatch_function`](#0x1_fungible_asset_withdraw_dispatch_function)
@@ -2532,6 +2533,33 @@ Return whether a fungible asset type is dispatchable.
 
 
 
+</details>
+
+<a id="0x1_fungible_asset_is_asset_type_dispatchable"></a>
+
+## Function `is_asset_type_dispatchable`
+
+Return whether a fungible asset type has any dispatch or derived-supply hooks registered.
+
+
+<pre><code>#[view]
+<b>public</b> <b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_is_asset_type_dispatchable">is_asset_type_dispatchable</a>(metadata: <a href="object.md#0x1_object_Object">object::Object</a>&lt;<a href="fungible_asset.md#0x1_fungible_asset_Metadata">fungible_asset::Metadata</a>&gt;): bool
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="fungible_asset.md#0x1_fungible_asset_is_asset_type_dispatchable">is_asset_type_dispatchable</a>(metadata: Object&lt;<a href="fungible_asset.md#0x1_fungible_asset_Metadata">Metadata</a>&gt;): bool {
+    <b>let</b> metadata_addr = <a href="object.md#0x1_object_object_address">object::object_address</a>(&metadata);
+    <b>exists</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_DispatchFunctionStore">DispatchFunctionStore</a>&gt;(metadata_addr) || <b>exists</b>&lt;<a href="fungible_asset.md#0x1_fungible_asset_DeriveSupply">DeriveSupply</a>&gt;(metadata_addr)
+}
+</code></pre>
+
+
+
 </details>
 
 <a id="0x1_fungible_asset_deposit_dispatch_function"></a>

@@ -0,0 +1,10 @@
+# --- Lean (`lean/`) ---
+# Lake cache lives under `lean/`; see `lean/.gitignore` for scratch/logs too.
+lean/.lake/
+
+# --- Rust difftest (`difftest/`) ---
+# VM oracle JSON emitted by `cargo run -p move-lean-difftest` / `difftest-stdlib.sh`
+difftest/difftest_oracle*.json
+difftest/difftest_merged.json
+difftest/difftest_ca_e2e_fragment.json
+difftest/difftest_ci_merged.json
@@ -0,0 +1,21 @@
+# Move formalization (stdlib-focused branch)
+
+- **Lean:** `lean/` — `MovementFormal` (MoveModel, `move-stdlib` specs, `lake exe difftest`).
+- **VM oracle:** `difftest/` — `move-lean-difftest` crate; stdlib-only driver: `difftest-stdlib.sh` (repo root).
+
+```bash
+./aptos-move/framework/formal/difftest-stdlib.sh
+```
+
+Prereqs: `elan` + Lean 4.24 (see `lean/lean-toolchain`), network once for `lake`/`mathlib` fetch.
+
+**Difftest methodology** (what the oracle is, how suites are registered, checklists): [`difftest/INVENTORY.md`](difftest/INVENTORY.md).
+
+## Docs (under `difftest/`)
+
+| File | What it is |
+|------|------------|
+| [`difftest/README.md`](difftest/README.md) | Harness overview: oracle JSON, `merge`, adding suites (parts are **CA-era**; stdlib-only workflow is `difftest-stdlib.sh` + `lake exe difftest`). |
+| [`difftest/INVENTORY.md`](difftest/INVENTORY.md) | How VM↔Lean difftest is meant to work (source of truth, suite registry checklist). |
+| [`difftest/ORACLE_CHANGELOG.md`](difftest/ORACLE_CHANGELOG.md) | JSON `schema_version` and compatible extensions (still the contract for parsers). |
+| [`difftest/STUB_POLICY.md`](difftest/STUB_POLICY.md) | Lean column policy (bytecode / natives / globals); **heavy confidential-asset context** — read for model background, not required for stdlib-only runs. |
@@ -0,0 +1,59 @@
+#!/usr/bin/env bash
+# Move ↔ Lean differential tests — **move-stdlib-related suites only** (no confidential / FA / e2e).
+#
+# Skips `verify-corpora` and `check_confidential_lean_hygiene.sh`. Oracle JSON contains only:
+#   vector, acl, bcs, bit_vector, error, hash, signer, string, cmp,
+#   fixed_point32, option, global_resource_smoke
+#
+# Usage (repo root):
+#   chmod +x aptos-move/framework/formal/difftest-stdlib.sh   # once
+#   ./aptos-move/framework/formal/difftest-stdlib.sh
+#
+# Optional: custom oracle path (absolute or relative to this script’s `difftest/` dir)
+#   ./aptos-move/framework/formal/difftest-stdlib.sh my_stdlib_oracle.json
+#
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+REPO_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+LEAN_DIR="$SCRIPT_DIR/lean"
+DIFTEST_CRATE="$SCRIPT_DIR/difftest"
+
+if [[ "${1:-}" == "-h" || "${1:-}" == "--help" ]]; then
+  sed -n '1,22p' "$0"
+  exit 0
+fi
+
+if [[ -n "${1:-}" ]]; then
+  if [[ "$1" == /* ]]; then
+    JSON="$1"
+  else
+    JSON="$DIFTEST_CRATE/$1"
+  fi
+else
+  JSON="$DIFTEST_CRATE/difftest_oracle_stdlib.json"
+fi
+
+STDLIB_SUITES=(
+  vector acl bcs bit_vector error hash signer string cmp
+  fixed_point32 option global_resource_smoke
+)
+
+SUITE_ARGS=()
+for s in "${STDLIB_SUITES[@]}"; do
+  SUITE_ARGS+=(--suite "$s")
+done
+
+echo "=== Move ↔ Lean differential tests (stdlib suites only) ==="
+echo "Oracle: $JSON"
+echo ""
+
+echo "[1/2] Oracle: cargo run -p move-lean-difftest → $JSON"
+(cd "$REPO_ROOT" && cargo run -p move-lean-difftest -- --quiet "${SUITE_ARGS[@]}" -o "$JSON")
+
+echo ""
+echo "[2/2] Lean: lake build difftest && lake exe difftest"
+(cd "$LEAN_DIR" && lake build difftest && lake exe difftest "$JSON")
+
+echo ""
+echo "Done."
@@ -0,0 +1,5 @@
+# Oracle / merge outputs (also listed in `../.gitignore` from repo `formal/` root).
+difftest_oracle*.json
+difftest_merged.json
+difftest_ca_e2e_fragment.json
+difftest_ci_merged.json
@@ -0,0 +1,40 @@
+[package]
+name = "move-lean-difftest"
+version = "0.1.0"
+edition = "2021"
+publish = false
+default-run = "move-lean-difftest"
+description = "Differential testing harness: runs Move functions through the real VM and exports JSON test vectors for the Lean evaluator to compare against."
+
+[lib]
+path = "src/lib.rs"
+
+[[bin]]
+name = "move-lean-difftest"
+path = "src/main.rs"
+
+[dependencies]
+anyhow = { workspace = true }
+bcs = { workspace = true }
+curve25519-dalek-ng = { workspace = true }
+hex = { workspace = true }
+sha2 = { workspace = true }
+sha3 = { workspace = true }
+aptos-cached-packages = { workspace = true }
+aptos-framework = { workspace = true }
+aptos-gas-schedule = { workspace = true }
+aptos-types = { workspace = true }
+aptos-vm = { workspace = true, features = ["testing"] }
+codespan-reporting = { workspace = true }
+move-binary-format = { workspace = true }
+move-compiler-v2 = { workspace = true }
+move-core-types = { workspace = true }
+move-model = { workspace = true }
+move-stdlib = { path = "../../../../third_party/move/move-stdlib" }
+move-vm-runtime = { workspace = true, features = ["testing"] }
+move-vm-test-utils = { workspace = true }
+move-vm-types = { workspace = true, features = ["testing"] }
+legacy-move-compiler = { workspace = true }
+serde = { workspace = true }
+serde_json = { workspace = true }
+tempfile = { workspace = true }
@@ -0,0 +1,55 @@
+# Difftest inventory & methodology (Phase 0)
+
+This document is the **hub** for planning and extending **Move VM ↔ Lean** differential tests (`move-lean-difftest` + `lake exe difftest`). It applies to **any** Move package you later wire into the harness (stdlib wrappers, framework modules, confidential assets, …).
+
+## 1. Source of truth — tests are allowed to fail
+
+- The **JSON oracle** is produced by running the **real Move VM** (Rust) on concrete inputs. Those outputs are treated as **ground truth for that run**.
+- The **Lean** side **re-computes** the same case using `MovementFormal.MoveModel` and **compares** to the oracle.
+- **If Move code is wrong** but Lean matches a *correct* spec, the VM oracle will still record what Move *actually* did — a **later** Lean change to match buggy Move would show as “passing” while being wrong. The intended discipline is:
+  - **Independent** expectations for high-value cases (e.g. golden vectors from crypto reviews, or second tooling), **or**
+  - **Regression**: when you **intentionally fix** Move, the oracle **must be regenerated**; Lean should then match the **new** VM behavior — a **failure** before regen catches drift.
+- **If Lean is wrong** (transcription, missing instruction, wrong native), comparison **fails** — that is the point of difftest.
+
+Neither implementation is assumed correct **by construction**; agreement is **evidence** on the oracle set only.
+
+## 2. Suite registry (generic harness)
+
+- **Rust:** one implementation of `DiffTestSuite` per logical area; register in [`src/suites/mod.rs`](src/suites/mod.rs) (`all_suites` + `suites_filtered` match arms — **keep match arms in sync** with `all_suites()`).
+- **List ids:** `cargo run -p move-lean-difftest -- --list-suites` or `./aptos-move/framework/formal/difftest.sh --list-suites`.
+- **Lean:** extend `MovementFormal.DiffTest.Runner` (`funcNameToMapping` / case dispatch) and `Move` `ModuleEnv` / natives for each **new** function you add to an oracle.
+
+See [`README.md`](README.md) § *Adding coverage* for the file-level checklist.
+
+## 3. Inventory artifacts (Phase 0 deliverables)
+
+| Document | Purpose |
+| -------- | ------- |
+| [`STUB_POLICY.md`](STUB_POLICY.md) | Lean column: bytecode vs natives vs abstract globals (CA plan §3). |
+| [`inventory/README.md`](inventory/README.md) | Index of per-package inventories. |
+| [`inventory/confidential_assets.md`](inventory/confidential_assets.md) | **Confidential assets (experimental)** — public API surface, difftest mode per symbol, native/transitive deps. Independent vectors (checklist §4.3 iii): [`corpora/confidential_assets/README.md`](corpora/confidential_assets/README.md). |
+| [`inventory/confidential_native_matrix.md`](inventory/confidential_native_matrix.md) | **CA native / crypto matrix** — `aptos_std` Ristretto/BP/hash vs Lean status (FV plan Workstream A). |
+| [`inventory/move_framework_template.md`](inventory/move_framework_template.md) | Blank template for **other** Move framework packages. |
+
+## 4. Difftest modes (per function / case)
+
+Use these labels in inventory tables:
+
+| Mode | Meaning |
+| ---- | ------- |
+| **VM↔Lean** | Full differential: oracle from VM, Lean `eval` must match. |
+| **VM-only** | Oracle recorded from VM; Lean column **skipped** until model exists (document reason). |
+| **Blocked** | Cannot run in harness yet (missing compiler support, storage, …). |
+
+## 5. When you add a new suite (checklist)
+
+1. Add `src/suites/<name>.rs` implementing `DiffTestSuite`.
+2. Register in `all_suites()` **and** the `suites_filtered` match in [`mod.rs`](src/suites/mod.rs).
+3. Run `cargo run -p move-lean-difftest -- --list-suites` and confirm the new id appears.
+4. Extend Lean `DiffTest` runner + `ModuleEnv` for each `TestCase` you emit.
+5. Add an **`inventory/<topic>.md`** row or standalone doc for long-term tracking.
+
+## 6. Related plans
+
+- Confidential assets **difftest-only** roadmap: [`../CONFIDENTIAL_ASSETS_DIFFERENTIAL_TESTING_PLAN.md`](../CONFIDENTIAL_ASSETS_DIFFERENTIAL_TESTING_PLAN.md) (Phase 0 marked complete there with pointer here).
+- Full formal verification (refinement + globals): [`../CONFIDENTIAL_ASSETS_FORMAL_VERIFICATION_PLAN.md`](../CONFIDENTIAL_ASSETS_FORMAL_VERIFICATION_PLAN.md).