Portable replay instructions and prerequisites
Sufficient Resolution
PORTABLE_REPLAY.md
1 # Portable serial replay
2
3 The proof runtime is supplied separately. This package contains proof sources,
4 finite companion code, source guides, historical verification and current
5 bounded evidence. It does not contain Lean executables or an imported Mathlib
6 build cache.
7
8 Required proof environment:
9
10 - Linux x86_64, including x86_64 WSL2 on Windows.
11 - Komorebi portable Lean 4.34.0-rc2, commit
12 `6a10ac8c22beadecabdbb0919c2b50214762f91d`.
13 - Mathlib revision `aeb72f1e9981b6d35b426b16dca7759be3e7ba06` and
14 dependency revisions in `lake-manifest.json`.
15 - Python with SymPy 1.14.0 for the finite companion cross-checks. Use
16 `requirements-rational-tests.txt`; Python is tested separately from Lean.
17
18 From this `formal` directory, inspect the source plan without a proof runtime:
19
20 ```bash
21 python3 scripts/verify.py --plan-only
22 ```
23
24 With the separately restored matching runtime, launch the full discovered
25 corpus serially:
26
27 ```bash
28 bash verify_low_memory.sh /path/to/Komorebi_Portable_Lean_4.34.0-rc2 \
29 --out verification/full93-local --timeout 240
30 ```
31
32 The driver requires exact Lean version/commit and dependency revisions. It
33 freshly compiles every discovered production module, builds the root, audits
34 every enumerated declaration, runs the stated negative controls, and replays
35 the production modules with the same Lean kernel. Imported Mathlib artifacts
36 are reused. The source parser is checked on this package and is not a general
37 Lean parser. A successful full runtime run has not been performed for this
38 edition.
39
40 The launcher sets one Lean thread, serial commands and a default per-process
41 address-space limit of 4 GiB. To choose a different limit, set
42 `KOMOREBI_VERIFY_MEMORY_KIB`. The limit is not aggregate process-tree memory.
43 The verifier has a per-command wall timeout. `--skip-kernel-replay` explicitly
44 reduces verification and is recorded in the report. It never means replay
45 passed.
46
47 From the release root, finite Python companions can be rerun without Lean:
48
49 ```bash
50 python3 verification/replay_finite_companions.py --plan-only
51 python3 verification/replay_finite_companions.py \
52 --output verification/local_python_replay
53 ```
54
55 Choose a new output directory for each run. The finite driver uses unchanged
56 check scripts in private per-suite trees, records native JSON results, and
57 validates bounded version-2 manifests. Each suite is capped at 600 wall
58 seconds, 500 CPU seconds per process, 1 GiB address space, one inherited core,
59 one cooperative numerical-library thread, and 1 MiB outer log output.
60 The fixed suites use their own documented seeds. Current bundled evidence
61 resides at `verification/python_replay`.
62
63 Validate a bundled manifest from the release root:
64
65 ```bash
66 python3 formal/scripts/provenance/validate_manifest.py \
67 verification/python_replay/calibration/manifest.json --root .
68 ```
69
70 The bundled provenance utilities are unchanged copies from mathbox
71 computation-audit 3.2.0. Their origin and hashes are recorded. Provenance
72 validation checks records and hashes. It does not prove the mathematics.