lean formal verification for move-stdlib

[ganymedio]

Move stdlib formalization + VM↔Lean difftest

Summary

stdlib-focused formalization of Move in Lean (MovementFormal): high-level specs, a bytecode-level MoveModel, and refinement proofs that connect the two. It also adds a VM↔Lean regression harness: a Rust tool drives the real Aptos Move VM, writes a JSON oracle of concrete outcomes, and a Lean executable replays those cases and checks agreement.

Workspace wiring (move-lean-difftest), docs under aptos-move/framework/formal/, and difftest-stdlib.sh (stdlib-only suites) are included so reviewers can lake build the proofs and run the difftest pipeline locally. Confidential-assets formalization, CA corpora, and CA-only difftest suites are not part of this change.

---

Contents of this PR

• aptos-move/framework/formal/lean/ — Lean 4 package MovementFormal: Std.* (move-stdlib-oriented lemmas), Refinement.Std.* (refinements against MoveModel), MoveModel.* (bytecode, catalogs, step lemmas), AptosStd.*, SmokeTests.*, DiffTest.* (oracle runner). Toolchain: lean/lean-toolchain (leanprover/lean4:v4.24.0). Lake roots are listed in lean/lakefile.lean; default library target is MovementFormal, executable difftest (lake exe difftest).
• aptos-move/framework/formal/difftest/ — Rust crate move-lean-difftest (workspace member): runs the Aptos Move VM, emits JSON oracle files.
• aptos-move/framework/formal/difftest-stdlib.sh — Runs stdlib-only VM suites then lake exe difftest on the generated oracle (same commands as below).
• aptos-move/framework/formal/README.md, aptos-move/framework/formal/.gitignore, and related ignores under lean/ / difftest/ — docs and ignore rules for generated artifacts (difftest_oracle*.json, .lake/, etc.).
• Cargo.toml / Cargo.lock — register move-lean-difftest in the workspace.

Refinements in this PR (MovementFormal.Refinement.Std.*)

What these are: Lean theorem files (Lake roots in lean/lakefile.lean). Most rows prove eval (the MoveModel interpreter) on a named env + native index + arguments equals the result of the matching MovementFormal.Std.* definition (or a tiny bytecode program wired to that spec). They are not Rust tests. The real VM is exercised separately by VM↔Lean difftests on finite oracles.

Lean module	What the theorems prove
MovementFormal.Refinement.Std.Bcs	Native.bcsToBytes_* and BcsCatalog helpers agree with MovementFormal.Std.Bcs (bcs.move primitives): per-type to_bytes encodings, serialized_size_*, vector<u8>, etc. — lean/MovementFormal/Refinement/Std/Bcs.lean.
MovementFormal.Refinement.Std.Core	For Programs.Core programs in stdModuleEnv, eval at fixed indices equals the spec on all inputs (e.g. add_u64, is_zero_u64, bcs_to_bytes_u64, read_via_ref, inc_via_ref, vec_push_and_len) — lean/MovementFormal/Refinement/Std/Core.lean.
MovementFormal.Refinement.Std.StdPrimitives	Bytecode from Programs.StdPrimitives in a single-function env (native index 8 after stdNatives) eval-matches Std.Error / Std.BitVector for the covered error::… / bit_vector::… shapes — lean/MovementFormal/Refinement/Std/StdPrimitives.lean.
MovementFormal.Refinement.Std.Vector	vector::contains as in Programs.Vector (native index 18 in stdModuleEnv) refines MovementFormal.Std.Vector.contains (loop + return; see file header for proof structure) — lean/MovementFormal/Refinement/Std/Vector.lean.
MovementFormal.Refinement.Std.Error	Each errorCatalogModuleEnv index 0–12 eval-matches the corresponding MovementFormal.Std.Error API (canonical, invalid_argument, …) — lean/MovementFormal/Refinement/Std/Error.lean.
MovementFormal.Refinement.Std.Hash	hashCatalogModuleEnv: native 0 = Std.Hash.Sha2_256, native 1 = Std.Hash.Sha3_256 on the same vector<u8> bytes — lean/MovementFormal/Refinement/Std/Hash.lean.
MovementFormal.Refinement.Std.Signer	signerCatalogModuleEnv: borrow_address / address_of eval-match MovementFormal.Std.Signer — lean/MovementFormal/Refinement/Std/Signer.lean.
MovementFormal.Refinement.Std.FixedPoint32Catalog	fp32Oracle* in MoveModel/Native/StdPrimitives return the same values as MovementFormal.Std.FixedPoint32 on the same oracle wires — lean/MovementFormal/Refinement/Std/FixedPoint32Catalog.lean.
MovementFormal.Refinement.Std.OptionCatalog	optionOracleU64* vs MovementFormal.Std.Option on Option<u64> scratch wires — lean/MovementFormal/Refinement/Std/OptionCatalog.lean.
MovementFormal.Refinement.Std.BitVectorCatalog	bitVector* natives vs MovementFormal.Std.BitVector on MvBitVector wires — lean/MovementFormal/Refinement/Std/BitVectorCatalog.lean.
MovementFormal.Refinement.Std.AclCatalog	aclOracle* vs MovementFormal.Std.Acl on MvAcl wires (e.g. empty ACL) — lean/MovementFormal/Refinement/Std/AclCatalog.lean.
MovementFormal.Refinement.Std.StringCatalog	eval on stringCatalogModuleEnv vs MovementFormal.Std.String on inputs aligned with stringOracle* — lean/MovementFormal/Refinement/Std/StringCatalog.lean.
MovementFormal.Refinement.Std.CmpCatalog	Concrete facts about MovementFormal.Std.Cmp (compareU64, compareBool, compareU8, compareAddress, compareU16/32/128/256, and isLt / isEq / …) on fixed argument pairs (rfl / native_decide). This file does not currently relate eval on CmpCatalogModuleEnv; it checks the pure comparison layer used alongside the cmp difftest suite — lean/MovementFormal/Refinement/Std/CmpCatalog.lean.

---

move-stdlib coverage (what this PR actually covers)

Source of truth for “stdlib” here: third_party/move/move-stdlib/sources (12 modules: bcs, hash, vector, signer, option, error, string, bit_vector, fixed_point32, type_name, ascii, unit_test).

Lean specs (MovementFormal.Std.*, Lake roots in lean/lakefile.lean) line up with most of those modules: BCS, hash (Keccak / SHA2-256 / SHA3-256), vector operations, signer, option, error (+ canonical error math), string / UTF-8, bit vector, fixed-point32, type_name, and Cmp (comparison helpers used with the cmp oracle path). MovementFormal.Std.ByteArrayAppend supports byte-level facts used alongside BCS/string-style reasoning.

Gaps / partiality relative to that 12-file tree:

• ascii.move — no separate Std/Ascii.lean; ASCII behavior is intended to sit under the string work, not a 1:1 file mirror.
• unit_test.move — not a formal verification target; no spec layer.
• Depth — coverage is spec + native catalogs + VM↔Lean difftests + selected refinement proofs, not “every public Move function has a completed refinement theorem.” Some Refinement.Std.* rows are catalog-only or fixed-point lemmas (called out in the table above).

Acl: MovementFormal.Std.Acl and matching catalogs/refinement exist for difftest and verification plans, but ACL is not one of the 12 third_party/move/move-stdlib sources; treat it as framework-adjacent surface area wired into the same harness.

---

Axioms — what would be required to remove them

Axioms are uneven: some are “finish the simp proof,” others are “whole sub-project.”

Bucket	Examples (see grep ^axiom under MovementFormal/)	Rough effort
Bytecode / small-step	Arithmetic.lean: step_eq_u64, step_neq_u64, step_eq_bool, step_neq_bool	Small: unfold step on .eq / .neq for non-reference scalars; case split on BEq / MoveValue (order of hours to a few days total, not crypto).
VM / container plumbing	ByteArrayLemmas.lean (address length, ByteArray extensionality-style facts)	Moderate: depends on how much ByteArray is unfolded vs kept abstract (days if proofs fight kernel reduction).
Composition & PC-chaining placeholders	PCChaining, NativeCallPatterns, OraclePatterns, BorrowFieldChains, CopyLocChains, ProvenChains, CopyLocChains.chain_five_moveLoc_two_copyLoc, …	Large: each name is a stand-in for a long run / step proof obligation (days per lemma, weeks+ if you drain the whole list systematically—or delete unused axioms if nothing imports them).
Crypto & curves	EdwardsCurve25519, RistrettoEncoding, Bulletproofs, Curve25519Field / Ristretto255 primality, …	Very large: these are external mathematics, not Move typing. Removing them means Mathlib (or similar) alignment, a small trusted axiom bundle, or weaker statements (weeks to months+ per area, not a single PR).

Practical takeaway: eliminating only the Arithmetic equality axioms and tightening ByteArray lemmas is realistic follow-up in this repo; eliminating every axiom including composition scaffolding and elliptic-curve / BP facts is a multi-track program (proof engineering + math), not a small cleanup.

---

Setup

• Rust: stable toolchain that builds this repo.
• Lean: elan. The compiler version is pinned in aptos-move/framework/formal/lean/lean-toolchain (Lean 4.24.x). The first time you use Lake from that directory it may clone Mathlib and other packages (network).

Before lake build: download Mathlib’s pre-built artifacts (otherwise Lean builds all of Mathlib from source — very slow). Run this exact command from aptos-move/framework/formal/lean/ (from repo root you can copy-paste the two lines as-is):

cd aptos-move/framework/formal/lean
lake exe cache get!

One line from repo root (same thing):

cd aptos-move/framework/formal/lean && lake exe cache get!

Details: aptos-move/framework/formal/lean/README.md.

---

lake build (Lean library + refinements)

Builds every Lake root in lakefile.lean (specs, MoveModel, Refinement.Std.*, smoke tests, difftest support code). From repo root (includes Mathlib cache step):

cd aptos-move/framework/formal/lean
lake exe cache get!
lake build

Build only the difftest executable (run lake exe cache get! first on a fresh checkout, same as above):

cd aptos-move/framework/formal/lean
lake exe cache get!
lake build difftest

---

VM↔Lean difftests

Option A — script (repo root). Run lake exe cache get! from aptos-move/framework/formal/lean/ at least once on a new machine (see Setup); the script does not run it for you.

chmod +x aptos-move/framework/formal/difftest-stdlib.sh   # once if needed
./aptos-move/framework/formal/difftest-stdlib.sh

Option B — same steps by hand (repo root for step 1):

cargo run -p move-lean-difftest -- --quiet \
  --suite vector --suite acl --suite bcs --suite bit_vector --suite error \
  --suite hash --suite signer --suite string --suite cmp \
  --suite fixed_point32 --suite option --suite global_resource_smoke \
  -o aptos-move/framework/formal/difftest/difftest_oracle_stdlib.json

cd aptos-move/framework/formal/lean
lake exe cache get!
lake build difftest
lake exe difftest ../difftest/difftest_oracle_stdlib.json

Expected: 471 passed, 0 failed, 1 skipped (test_read_std_counter / borrow_global, skip_lean).

Oracle JSON under difftest/ is gitignored; regenerate with step 1 before running Lean.

---

Optional: compile the Rust oracle tool (no Lean)

If you only want to confirm the move-lean-difftest crate typechecks in the workspace—without lake, Mathlib, or lake exe difftest—from repo root:

cargo check -p move-lean-difftest