ProofForgeCommon

Shared ProofForge surface for the target compiler repositories (ProofForgeEvm, ProofForgeSvm, ProofForgeNear, ProofForgePsy).

Single source of truth for:

• ProofForge.Attr — pf_entry / pf_inline / pf_boundary tag attributes
• ProofForge.Core.* — target-neutral IR, Ops, CFG, projection (Core.Target), codec, schema, value, math, fixed-point, collections, safe-cast, eval, except
• ProofForge.Crypto.* — Sha256 / Keccak (host + source-level semantics)
• ProofForge.Quint.* — default target: extension-free dialect (ProofForge.Quint.Ops), the default Core.Target.Registration, and a source-only Quint (.qnt) emitter for hand-built Core programs
• ProofForge.Profile — compile-root profile checks

Depends on Lean + Std only. No Mathlib, no target SDKs, no extractors. Module paths mirror the consumer repositories (ProofForge/Core/Codec.lean …), so import ProofForge.Core.* keeps working unchanged after a target repo switches to require «proofforge-common».

Layout

ProofForge/            shared library (lean_lib ProofForgeCore)
ProofForgeCoreTests/   pure-Core specs (CoreCodecSpec, CoreCollectionsSpec, CoreMathSpec, QuintSpec)

Target-specific layers (target Runtimes, SDKs, extractors, CLI, and extended attributes such as pf_svm_raw*) stay in the target repositories.

Consuming

require «proofforge-common» from git
  "https://github.com/DaviRain-Su/ProofForgeCommon.git" @ "main"

Tracking main means a push here reaches the consumer repositories on their next build — no tag dance. main is branch-protected (the Lean CI check must pass), so a breakage is caught in this repository's CI before consumers ever see it; the consumers' CI doubles as the integration test.

For a reproducible build (e.g. a release), a consumer may pin a commit SHA or a milestone tag instead; tags are cut manually for especially large features.

lean-toolchain here is pinned to the same version as the consumer repositories; bump all five together.

Development

lake build                       # builds ProofForgeCore only
lake build ProofForgeCoreTests   # builds every spec module (what CI runs)