8000 Record protected corpus export evidence by Mnehmos · Pull Request #56 · Mnehmos/MathOS · GitHub
[go: up one dir, main page]
Skip to content

Record protected corpus export evidence #56

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mnehmos merged 1 commit into from
Jul 22, 2026
Merged

Record protected corpus export evidence #56

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/implementation/RELEASE_CHECKLIST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ Phase 5 evidence: issue [#48](https://github.com/Mnehmos/MathOS/issues/48) adds

Phase 6 portable-release evidence: issue [#50](https://github.com/Mnehmos/MathOS/issues/50) adds the closed Rust-owned `release_manifest/1` schema and a deterministic dry-run/new-directory builder rooted in one fully replayed publication receipt plus its persisted authority/current fidelity witness and one exact reviewed pedagogy path. Every required SPEC directory has manifest-bound members; exact record, logical/pedagogy edge, evidence, artifact, environment, publication, replay, report-copy, and license relationships are checked without SQLite. Private members retain explicit restrictions, and the public release profile rejects any restricted, private, or unlicensed member. Unit coverage reproduces the preview hash after restart, blocks overwrite and public projection, hides SQLite, revalidates the directory, and rejects extra files, expected-hash substitution, and a changed export. The protected Pilot A workflow builds five reviewed training-ineligible units, copies the resulting release, hides `state.sqlite3`, invokes verification with a nonexistent instance root and trusted manifest hash, replays the exact repaired theorem under Lean 4.32.0, and retains both bundle and report.

Phase 6b corpus-export evidence: issue [#54](https://github.com/Mnehmos/MathOS/issues/54) pins the byte-exact Apache-2.0 MathCorpus packet and minimum MCIP v1 schemas at upstream commit `a0d08c9ace0dcc70a8bc281dcf29c560242075d3`, adds the closed Rust-owned `corpus_export_manifest/1` contract, and exposes database-independent `mcl release export` and `verify-export`. Classification is explicit rather than guessed. Private releases produce only `private_audit_only` packets, `private_only` MCIP records, and private sensitive members; public releases remain quarantined and additionally require explicit public redistribution, redaction, and license authority. Verification checks a trusted export hash, exact inventory and schemas, canonical packet/record hashes, source/publication/environment/module bindings, and byte-identical deterministic reprojection from an independently supplied frozen release. Unit and CLI coverage blocks overwrite, missing-root/config coupling, invalid curation, extra files, and schema substitution. A Windows CLI playtest projected the retained protected Pilot A release `0417d31249de47d49609913e79021b6a8ba9ec265105a057a29237337c30913d` to export `33e6ccc24979e85c14688d755130ace9960f0e074342695e951ac9756c2c590b`; offline reprojection passed, and upstream MathCorpus and MCIP validators reported zero errors and zero warnings with hash checking enabled. The protected workflow now repeats dry-run, build, copy, and verification while SQLite is hidden. RL/evaluation export, leakage-aware splits, Comparator, remaining pilots, and full 1.0 acceptance remain unfinished.
Phase 6b corpus-export evidence: issue [#54](https://github.com/Mnehmos/MathOS/issues/54) and PR [#55](https://github.com/Mnehmos/MathOS/pull/55) pin the byte-exact Apache-2.0 MathCorpus packet and minimum MCIP v1 schemas at upstream commit `a0d08c9ace0dcc70a8bc281dcf29c560242075d3`, add the closed Rust-owned `corpus_export_manifest/1` contract, and expose database-independent `mcl release export` and `verify-export`. Classification is explicit rather than guessed. Private releases produce only `private_audit_only` packets, `private_only` MCIP records, and private sensitive members; public releases remain quarantined and additionally require explicit public redistribution, redaction, and license authority. Verification checks a trusted export hash, exact inventory and schemas, canonical packet/record hashes, source/publication/environment/module bindings, and byte-identical deterministic reprojection from an independently supplied frozen release. Unit and CLI coverage blocks overwrite, missing-root/config coupling, invalid curation, extra files and directories, packet/schema substitution, and expected-hash substitution. Exact-head CI `29884823358`, merged-tree CI `29885040172`, and protected publication run `29885040178` passed. Downloaded artifact `8516235885` independently reproduced source release `7b002ffe0fcaeecd0fe745dcedd135442b7372985a0fac5b9ffbe03af4c691b1`, corpus manifest `4cb348d8a446f800d74865909c8fff66b310c5cd0fbe6fb00f6830d0961ed705`, and packet `690d7f8a18fad1fee415b5d6ad4efeaf154a2a7dc366b892967230d49db6c69d`; all 12 files and 11 manifest members matched, no links existed, deterministic reprojection passed without SQLite, and upstream MathCorpus and MCIP validators reported zero errors and warnings with hash checks enabled. RL/evaluation export, leakage-aware splits, Comparator, remaining pilots, and full 1.0 acceptance remain unfinished.

## Migration

Expand Down
10 changes: 6 additions & 4 deletions docs/implementation/STATUS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,9 @@ Issue [#48](https://github.com/Mnehmos/MathOS/issues/48) completed the narrow Ph

Issue [#50](https://github.com/Mnehmos/MathOS/issues/50) completed the first Phase 6 portable-release slice through PR #51 plus policy corrections #52 and #53. Merge `84987c70c01ce8f61db7af1346883571b7b34868`, tree `1868ef4c3e0e9321788c3685665fbc37486da3b7`, passed main CI run `29881189890` and protected publication run `29881189881`. The closed `release_manifest/1` contract, deterministic no-write preview, immutable directory build, explicit member licensing/restrictions, public fail-closed profile, and database-independent structural plus Lean replay are live. The retained protected artifact contains five reviewed training-ineligible units, all required release families, and an exact private release with manifest `0417d31249de47d49609913e79021b6a8ba9ec265105a057a29237337c30913d`; independent audit matched all 83 manifest members and replayed its authority, fidelity, receipt, environment, and repaired theorem bindings.

Issue [#54](https://github.com/Mnehmos/MathOS/issues/54) is the current focused Phase 6b slice. It vendors the minimum byte-exact MathCorpus and MCIP v1 schemas at upstream commit `a0d08c9ace0dcc70a8bc281dcf29c560242075d3`, adds the closed `corpus_export_manifest/1` contract, and implements database-independent `release export` and `verify-export`. The exporter follows only exact frozen source, claim, formalization, receipt, authority, fidelity, environment, and module bindings. Private releases remain `private_audit_only`/`private_only`; public releases remain quarantined until leakage-aware splits and require explicit public source and module license authority. The verifier denies unpinned schema retrieval, checks canonical packet and MCIP hashes, rejects inventory/schema/path substitution, and requires byte-identical reprojection from an independently supplied frozen release. A Windows CLI playtest over the retained protected Pilot A release produced export manifest `33e6ccc24979e85c14688d755130ace9960f0e074342695e951ac9756c2c590b`; MathOS offline reprojection and upstream MathCorpus/MCIP hash validators all passed with zero findings. Protected merged-tree evidence is still required before #54 closes. RL/evaluation export, leakage-aware splits, Comparator, remaining pilots, and full 1.0 acceptance remain unfinished.
Issue [#54](https://github.com/Mnehmos/MathOS/issues/54) completed the focused Phase 6b slice through PR [#55](https://github.com/Mnehmos/MathOS/pull/55). Reviewed head `55711785dd8ed9303bd54a0e7f6308efdead8ad7` merged as `e977d7eb69bfc262510c276912ba5584f3514a44`, tree `5c65154dd7f45497ba8ed1f06820ca3332ee9a7d`. Exact-head CI run `29884823358` and merged-tree CI run `29885040172` passed all five required jobs. Protected publication run `29885040178`, job `88813765985`, passed the protected-ref gate, authority/fidelity chain, repaired proof, portable release, database-hidden corpus preview/build/copy/reprojection, and retention.

Artifact `8516235885`, `publication-boundary-e977d7eb69bfc262510c276912ba5584f3514a44`, is 417,954 archive bytes with GitHub SHA-256 `55b4342eb03d19941d73086b6c44aae5083c834f824205a6138c7ddcdfe7d1d4`; it expands to 325 files and 770,532 bytes. Independent audit matched all 12 corpus-directory files, all 11 manifest member hashes and sizes, found no symbolic links, and confirmed byte-identical copied source manifest and Lean module. Source release `7b002ffe0fcaeecd0fe745dcedd135442b7372985a0fac5b9ffbe03af4c691b1` reprojected exactly to corpus manifest `4cb348d8a446f800d74865909c8fff66b310c5cd0fbe6fb00f6830d0961ed705`, packet `690d7f8a18fad1fee415b5d6ad4efeaf154a2a7dc366b892967230d49db6c69d`, 11 members, and 101,695 member bytes. The retained preview, build, verification, and playtest summary agree; MathOS offline verification and the pinned upstream packet and MCIP hash validators reported zero findings. RL/evaluation export, leakage-aware splits, Comparator, remaining pilots, and full 1.0 acceptance remain unfinished.

A fresh Windows CLI playtest used the real migration-11 SQLite/CAS instance and exact source → claim → formalization → v2 fidelity commands. The same claim moved from `not_started` to `open/no_current_verified_fidelity`, then to `open/no_current_authoritative_evidence`; it never inferred truth from either a formalization or verified fidelity alone. Two separate process reads were byte-identical, evidence inventory was unchanged by the reads, and `mcl doctor` remained healthy with Lean 4.32.0 visible. The protected merged-tree artifact separately records `open/no_current_verified_fidelity` after formal authority and `proved` only after role-separated verified v2 fidelity.

Expand Down Expand Up @@ -238,8 +240,8 @@ These items establish only part of the product foundation and trace model. One e

## Next highest-priority criteria

1. Complete issue #54 through exact-head review, protected merged-tree corpus-export playtest, and independent retained-artifact audit.
2. Implement leakage-aware RL/evaluation splits without promoting private, quarantined, benchmark, or held-out evidence.
1. Implement leakage-aware RL/evaluation splits without promoting private, quarantined, benchmark, or held-out evidence.
2. Define the Comparator package boundary from frozen evidence without granting authority.
3. Continue the remaining pilots and section 30 criteria without treating this partial path as MathOS 1.0.

## Exact last validation commands
Expand Down Expand Up @@ -286,4 +288,4 @@ Observed validation evidence for this update:

## Release readiness

Not ready. Protected Pilot A authority, fidelity, repair, pedagogy, portable-release, and local corpus-export evidence exist, but the merged-tree #54 artifact audit, leakage-aware RL/evaluation exports, Comparator, remaining pilots, later interfaces, and many section 30 criteria are still unfinished.
Not ready. Protected Pilot A authority, fidelity, repair, pedagogy, portable-release, and corpus-export evidence exist, but leakage-aware RL/evaluation exports, Comparator, remaining pilots, later interfaces, and many section 30 criteria are still unfinished.
Loading
0