# ML-VIC-001 — Reproducibility guide (English)

This is an English translation of the supplied REPRODUCE.md, edition 1.0. No new Lean or Anvil run is claimed.

## 1. Check the original evidence package

Unpack the original evidence archive into its own directory and run from that package root:

```sh
python3 tools/verify_package.py
```

Expected: PACKAGE_INTEGRITY_OK. It checks files, sizes and SHA-256 against the unsigned manifest; 15 original Git blob IDs, 12 included inputs matching the historical 115-hash list, and 157 runtime bytes. This is not a signature, authorship authentication or Lean check. Do not run this against the adapted website directory: English additions are not in the original manifest.

## 2. Export the full pinned source

Python 3.10+ and Git with authorized private-repository access are needed. Subsequent bootstrap requires Python 3.12+. Use the configured credential helper or an existing clone; never put tokens in URLs or command arguments.

```sh
python3 tools/build_source_bundle.py --repo-root /path/to/vickrey-lean-solidus
# Or clone using existing Git authentication:
python3 tools/build_source_bundle.py
```

Output: vickrey-source-d02ea87.zip and a separate provenance JSON. Commit d02ea87ce713d589c72328b89902a92d11275480; tree da1a82df7e4612091f2996fea7ffc1d8b33cb01b. If absent in the clone, run git fetch origin codex/verify-refinement, then repeat. The tool uses git archive of that commit, checks all 115 historical inputs and 15 supplied originals, rejects unsafe paths/symlinks, excludes .git, credentials and uncommitted changes, and refuses to overwrite an existing ZIP. It does not change branches, push, or run Lean. Remote export was not tested here.

## 3. Run a new proof check

Use the full source archive, not source-excerpts. The source recommends macOS arm64, Python 3.12+, Git, Xcode CLI and elan. Lean is selected by lean-toolchain. Cold builds need network, several GB disk and, according to the source README, about 5 GB RAM for one certificate.

```sh
cd vickrey-source-d02ea87
cp -R results ../recorded-results-d02ea87
cp versions.json ../recorded-versions-d02ea87.json
cp lake-manifest.json ../recorded-lake-manifest-d02ea87.json
make bootstrap
make verify
```

Bootstrap fetches pinned dependencies and macOS arm64 tools. On Linux, install the required solc/forge/cast/anvil into PATH first; this publication does not establish successful Linux reproduction. Bootstrap may update lock/metadata files: inspect changes and keep new logs separate from the historical release. Solidus is installed to vendor/solidus. Third-party dependencies and executables are not bundled.

Pins: Lean 4.28.0; solc 0.8.26+commit.8a97fa7a; Foundry 1.5.1. Dependency Git revisions are in versions.json and lake-manifest.json. A successful new make verify must exit 0 and produce a new VERIFIED record for the same explicitly stated boundary. Preserve new logs, versions and results as a separate release. Do not carry the old badge to modified sources.

make artifacts explicitly regenerates artifacts; it is not required for the first replay of committed files. make verify-economics checks only a subset, not the entire runtime. make negative-proof repeats a separate formal mutation regression. Legacy diagnostics are expected not to achieve full success and do not replace the main gate.

Even a successful rerun does not expand the boundary: selected structured AST, exact runtime, valid bids and the specified fresh ABI frame only. OutOfGas is allowed. A sufficient successful gas limit, deployment, transaction reachability, ETH transfers, escrow and commit/reveal strategic properties remain unestablished.

## 4. Package tools

```sh
python3 -B tools/test_package_tools.py
```

The packaging record reports 8 offline tests of blob IDs, traversal/symlink rejection, safe tar, source hashes, deterministic ZIP/no overwrite and export without uncommitted/secret files. They do not run proofs or auction tests. In this website adaptation on Windows, 6 passed, a symlink test was blocked by OS privilege and a Git export test failed on CRLF/LF conversion. The original recorded 8-test result is preserved as historical evidence, not presented as reproduced here.