sail-phase2-bootstrap

Sail-zkVM integration — Phase 2 bootstrap (foundation migration)

Historical bootstrap record. Current maintenance moved to Verified-zkEVM/riscv-zkvm.

For: the next session. Goal of P2: vendor the (now-proven) current-upstream scoped RV64IM Lean model into evm-asm, build it in-project, drop the moving dhsorens fork, and re-establish the 51 *_sail_equiv lemmas against it.

Status (2026-06-25): steps 1–4 DONE — the core P2 migration is complete and green. dhsorens is gone from lakefile.toml/lake-manifest.json; the project builds against the vendored model (require out from "vendor/sail-riscv-zkvm-lean"). Full lake build EvmAsm = 2984/2984, exit 0. All 51 *_sail_equiv lemmas green; axioms = {propext, Classical.choice, Quot.sound} only (no custom axioms, no sorryAx); no forbidden tactic in vendored or proof code. The LeanRV64D → Out rename was 100% mechanical — the feared bool_to_bit → bool_to_bits rename was a PHANTOM (both old and new model use bool_to_bit; the doc below had it backwards). Residual P2 items 5–7 (config revalidate, scoping write-up, pin gate) are tracked below and in docs/agents/sail-phase3-bootstrap.md; none block downstream proof work.

What proved out (the two real risks, both retired):

• lean-sail v4 + mathlib-master coexist in the real evm-asm build (StateRel + 2984-job full build). This was the one unverified step-1 risk.
• The 51 lemmas re-point with zero genuine logic renames — pure LeanRV64D → Out.

Read first: sail-import/PROVENANCE.toml [target] (the proven pins + vendor_path

• model_sha256). Then scripts/regen-sail-model.sh (the validated regen recipe) and docs/agents/sail-regen-spike.md (the GO report) only if you need to regenerate.

Proven foundation (DONE — don't re-litigate)

• Toolchain stack: Sail 0.20.2 (opam switch sail5, OCaml 5.4.1 — 4.14.2 stack-overflows, sail#1674) + sail-riscv release tag 2026-06-22-b5a2182 + external lean-sail v4 (79b4d08) on lean4 v4.30.0-rc1 (NO bump). z3 4.15.3 at the nix path in regen-sail-model.sh (machine-specific — de-nix before CI).
• Generation works (step ✔): scripts/regen-sail-model.sh --run <dir> → 113 files, scoped main I_insts M_insts, decode bv_decide-free.
• Matched pair builds (step ✔): that model + lean-sail v4 → lake build 84/84, exit 0.
• VENDORED + re-proven from git (step 2, commit a2dedf448): vendor/sail-riscv-zkvm-lean/ (113 .lean, package out, lib Out). Its lakefile.toml git-pins lean-sail @ 79b4d08 (tag v4); lean-toolchain = v4.30.0-rc1. A clean lake build from the committed dir — fetching lean-sail fresh from the pinned rev — gives 84/84, exit 0. model_sha256 recorded in PROVENANCE. Package/lib names kept verbatim from the proven artifact (renaming the lib would rewrite every internal import Out.*).