Repository navigation
Phase 6a: portable release bundle and offline replay gate #50
Description
Context
MathOS 1.0 now has canonical pedagogy through #48/PR #49, but the protected publication artifact still contains no pedagogy or portable release projection. SPEC §§19–20 require canonical state to freeze into a hashed release that verifies after the operational SQLite database is unavailable. Corpus/RL exports must derive only from such a frozen release.
This issue is intentionally limited to the Phase 6a release foundation. MathCorpus/MCIP serialization, RL task families, leakage-aware splits, and Comparator packages remain follow-up slices built on this bundle.
Scope
- Define a closed, bounded Rust-owned
release_manifest/1contract and committed JSON Schema with deterministic identity, explicit profile, exact root identities, sorted path-safe file inventory, hashes, sizes, licenses/restrictions, and replay metadata. - Build one portable release from an exact receipt-bound authoritative publication candidate plus an explicit exact reviewed pedagogy path.
- Materialize the SPEC minimum layout:
manifest.json,objects/,edges/,evidence/,artifacts/,environments/,licenses/,replay/,reports/, andexports/. - Revalidate current canonical publication authority, learning-unit references/edges/content, review state, and license policy immediately before materialization.
- Support private/internal bundles with explicit restrictions; make public profile fail closed on any unresolved, restricted, stale, nonpublic, or training-ineligible member.
- Verify a copied bundle without opening the operational database: reject unsafe paths, missing/extra files, hash/size/schema/reference/license drift, and replay the exact Lean artifact under its pinned environment before reproducing the same manifest hash.
- Expose deterministic dry-run/build/verify through one shared application service and first-class CLI release family. Keep arbitrary shell and caller-chosen replay commands out of the interface.
- Extend the protected Pilot A workflow to retain a private portable release containing its exact proof/refutation state and reviewed pedagogy path, then verify it with the workflow database hidden.
Acceptance criteria
-
release_manifest/1denies unknown fields, bounds every collection/string/size, uses closed enums, requires strictly sorted unique canonical paths, and has a committed schema equality/golden-hash test. - Build output contains every required top-level directory and only manifest-listed regular files; temporary/partial output is never accepted as a release.
- Every included record, edge, evidence item, environment, and artifact is exact and content-addressed; the manifest binds the authoritative publication receipt and exact reviewed pedagogy root/path.
- License inventory records either a resolved license or an explicit restriction for every exported member. Public build rejects any incompatible/unresolved license, nonpublic redaction/restriction, stale reference, or learning unit not
eligible_public. - Build is deterministic across process restart and clean destination roots; dry-run writes nothing; existing nonempty destinations and traversal/symlink inputs fail closed.
- Offline verify succeeds after copying the bundle and hiding/removing the operational database, rehashes every byte, revalidates canonical documents and internal references, executes only the pinned typed Lean replay, and reproduces the manifest hash.
- Single-byte corruption, missing/extra files, manifest substitution, unsafe paths, wrong receipt/pedagogy identities, and replay failure are rejected with structured errors.
- CLI tests and the protected Pilot A run build and offline-verify a private release containing source, claim, formalization, authority/fidelity evidence, logical graph, pedagogy graph, learning content, environment, reports, licenses/restrictions, and replay instructions.
- Status/checklist documentation records exact evidence and explicitly leaves MathCorpus/MCIP, RL/evaluation export, leakage splits, and Comparator support open.
Verification
cargo fmt --checkcargo clippy --workspace --all-targets --all-features -- -D warningscargo test --workspacePYTHONPATH=src PYTHONWARNINGS=error::ResourceWarning python -m unittest discover -s tests -v- focused real CLI build/copy/hide-database/verify/corrupt playtest
- protected merged-tree release build and independent artifact audit
git diff --check
Activity
Mnehmos commentedon Jul 22, 2026
Completed and independently audited on protected main.
Implementation and gates:
Portable release result:
Authority and replay bindings:
All acceptance evidence for #50 is now closed.