Skip to content

FORK.md

Latest commit

 

History

History
38 lines (26 loc) · 2.03 KB

FORK.md

File metadata and controls

38 lines (26 loc) · 2.03 KB
Raw

Fork Notes

starlib is a continuation of ArkLib, the Lean 4 formalization effort by the verified-zkEVM project. This document records the relationship between the two repositories.

Origin

starlib was initialized from a snapshot of ArkLib's main branch. The full repository contents — Lean sources, blueprint, knowledge base, scripts, and CI — were carried over and renamed:

Upstream identifier starlib identifier
ArkLib/ directory Starlib/
ArkLib.lean root module Starlib.lean
import ArkLib.… import Starlib.…
Lake package Arklib Lake package Starlib
Lake library ArkLib Lake library Starlib

URLs that point to the upstream project (for attribution or historical reference) are preserved as https://github.com/Verified-zkEVM/ArkLib.

What carried over unchanged

  • The mechanized theory of Interactive Oracle Reductions and all OracleReduction/, ProofSystem/, CommitmentScheme/, and Data/ modules.
  • The blueprint sources under blueprint/src/ (LaTeX prose and bibliography).
  • The knowledge base under docs/kb/ and the agent wiki under docs/wiki/.
  • The validation, linting, and timing scripts under scripts/.
  • The full CI matrix under .github/workflows/.
  • The license and author list (see LICENSE and AUTHORS).

What changed in this fork

  • Module / library / package name renamed to Starlib (and starlib where lowercased).
  • README rewritten to introduce starlib and link back to ArkLib for attribution.
  • A new docs/getting-started.md is provided for newcomers.

No theorem statements, proofs, or protocol formalizations were altered as part of the rename.

Acknowledgements

All credit for the original formalization, protocol coverage, and design effort belongs to the ArkLib authors and contributors listed in AUTHORS. starlib exists thanks to their work, and continues development in the spirit of the same upstream community.