Alternative Review Plan and Milestone Restructuring: Halo 2 / Orchard Lean 4 FV
This post is motivated in part by some of the discussion around this grant from the May 11th meeting.
I’m proposing a restructure of the milestones below in two ways: a Phase 1 milestone swap that pulls the ECC gadget to M1, and a Phase 3 reframe that replaces the two report-style deliverables with formal Lean 4 theorems. Total scope, total duration, and total budget are unchanged.
Change 1: M1 / M2 swap (ECC first)
The ECC gadget (variable-base scalar multiplication, fixed-base scalar multiplication, incomplete addition on the Pallas curve) is the single hardest item in Phase 1, as the original proposal already acknowledges in its risk-mitigation language. The original placed ECC at M2 alongside Merkle and RangeCheck; this revision pulls ECC forward to M1.
LookupRangeCheck is already complete (https://github.com/MavenRain/halo2-formal) and will be delivered at grant start, not as part of M1, so M1 carries only the ECC gadget.
Change 2: Phase 3 formal deliverables (not reports)
The original Phase 3 milestones (M5 post-quantum migration analysis, M6 privacy extensions) ended in technical reports. Under the same front-loading principle, this reads as a soft end. This revision rewrites both deliverables as formal Lean 4 artifacts:
- M5 produces formal Lean theorems on which Orchard protocol properties survive a transition to a lattice-based or hash-based proof system, with the supporting compatibility model expressed as a typed structure. The accompanying technical report becomes a reading guide to the formal artifact, not the artifact itself.
- M6 produces a formal Lean security model for cross-chain shielded transfers and a formal analysis of alternative key-exchange mechanisms for note encryption. Again, the report becomes a reading guide.
The research surface stays the same; the deliverable becomes a verifiable artifact rather than prose.
Revised month-by-month plan
| Month | Deliverable |
|---|---|
| 1 | ECC: variable-base scalar multiplication specification and completeness proof setup |
| 2 | ECC: soundness proof, including incomplete-addition edge cases |
| 3 | ECC: fixed-base scalar multiplication and integration. Milestone 1 (ECC complete; LookupRangeCheck delivered at grant start) |
| 4 | Sinsemilla: Pallas-based hash specification and Merkle integration setup |
| 5 | Sinsemilla: soundness and completeness proofs |
| 6 | Poseidon / Pow5: round-function constraints. Milestone 2 (Sinsemilla + Poseidon + Phase 1 technical report) |
| 7 | MerklePath: formalization (depends on Sinsemilla, complete at end of M2) |
| 8 | Orchard protocol formal model from ZIP 224 |
| 9 | Spend authorization and balance formal proofs. Milestone 3 |
| 10 | Fiat-Shamir soundness: transcript binding, Frozen-Heart class analysis |
| 11 | Binding signature verification and value balance |
| 12 | Note encryption correctness. Milestone 4 (ePrint preprint submitted) |
| 13 | Post-quantum migration: formal compatibility model as Lean structures; candidate-system survey |
| 14 | Post-quantum migration: formal Lean theorems for Orchard properties surviving lattice / hash transition |
| 15 | Post-quantum migration: new-assumption proofs and reading-guide report. Milestone 5 |
| 16 | Privacy extensions: cross-chain shielded-transfer formal security model |
| 17 | Privacy extensions: alternative key-exchange formal analysis |
| 18 | Final integration and presentation. Milestone 6 (final code release, presentation) |
The plan front-loads the most novel curve and hash work in months 1 through 6, places the protocol-level glue in months 7 through 12, and ends with the formal research deliverables that the original proposal carried as reports. Each month closes with an artifact in the public repository for asynchronous review between milestone boundaries.
Reviewer engagement plan
Daira Emma offered help and endorsed the proposal at the April 30th call, and Conrado confirmed on the same call that the Zcash Foundation has zero formal-verification bandwidth and welcomes outside contributors. I am grateful for both signals. I will coordinate per-milestone review with Zcash core developers, sharing work in progress between milestones for asynchronous review and requesting sign-off at each milestone boundary. Out of respect for everyone’s time, I will hold off on naming specific reviewers in public until they have agreed to take on particular milestones, and I will report each sign-off back to the committee as it comes in.
Acceptance of expert-review payment cadence
Milestone payments are contingent on expert review and may delay for reasons outside ZCG’s control. The work will continue while reviews are in flight, and I do not expect ZCG to compensate for review delays. I will budget cashflow accordingly.
Available for the next Arborist Call
I am available to present this restructured plan on a call, if needed, or to respond in writing to any further committee questions. The LookupRangeCheck repository, the methodology writeup, and the in-progress Lean 4 source are all open at https://github.com/MavenRain/halo2-formal for committee review at any time.
Onyeka (Oni) Obi (aka MavenRain)