小さな信頼基盤
信頼の説明は、source generation や navigation metadata ではなく、canonical certificate bytes と checker output から始めます。
Nano Proof Auditor
数学パッケージのための、証明書優先の証明検証。
NPA は、検査済みの証明書証拠と、便利ではあるものの信頼境界の外にあるメタデータを明確に分けます。このページでは、ツールチェーン、信頼モデル、finitefield.org/npa/ 配下のパッケージURLを紹介します。
NPA tag
v0.1.1
npa-site catalog の package toolchain pin。
Rust
1.95.0
移植元サイトが記録している toolchain version。
Packages
2
npa-mathlib と npa-std を /npa/ 配下に公開。
Theorems
750
npa-mathlib から表示する現在の theorem count。
Pinned toolchain
NPA_GIT_TAG = v0.1.1
RUST_TOOLCHAIN_VERSION = 1.95.0
パッケージ監査の導線
パッケージページでは、version、license、module count、theorem count、verification commands を安定したURLで示します。
数学定理の公開基盤
今後 npa-mathlib の定理紹介を増やすときは、推奨した数学URL構造の下に theorem page を追加できます。
Trust boundary
検査済み証拠と sidecar を意図的に分けます。
NPA互換リポジトリには source files、replay data、theorem indexes、reports を含められます。信頼境界は検査済み certificate path であり、その他は discovery、review、navigation の補助です。
Certificates and checker results
verifier output と .npcert files を、数学的な checking evidence として扱う artifact にします。
Metadata and replay data
meta.json、replay.json、indexes、generated navigation files は proof inspection を助けますが、checker boundary そのものではありません。
Package URLs
/npa/ 配下では、短くブランド所有の package path を使います。
URL戦略では NPA を研究ブランドかつ会社の長期資産として扱うため、パッケージページは generic な OSS セクションではなく finitefield.org/npa/ 配下に置きます。
npa-mathlib
形式化数学ライブラリ
npa-site catalog から、現在 61 modules と 750 theorem entries を表示する公開 theorem-library package です。
0.1.27
Version
61
Modules
750
Theorems
npa-std
標準論理・算術パッケージ
NPA互換パッケージが使う logic and arithmetic primitives のために、standard package path を /npa/std/ に確保します。
0.1.0
Version
2
Modules
MIT
License
Local audit
パッケージ紹介の横に verification commands を残します。
移植元サイトは NPA を local auditing workflow として見せています。この運用感を会社サイト側にも残します。
Certificates を監査
npa package verify-certs --root ../npa-mathlib --checker reference --jsonPackage policy を検査
npa package check --root ../npa-mathlib --json