8000 docs: record protected Comparator package evidence by Mnehmos · Pull Request #62 · Mnehmos/MathOS · GitHub
[go: up one dir, main page]
Skip to content

docs: record protected Comparator package evidence #62

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

docs: record protected Comparator package evidence #62

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
6 changes: 4 additions & 2 deletions docs/implementation/RELEASE_CHECKLIST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,9 +108,11 @@ Phase 6b corpus-export evidence: issue [#54](https://github.com/Mnehmos/MathOS/i

Phase 6c leakage-aware RL/evaluation evidence: issue [#57](https://github.com/Mnehmos/MathOS/issues/57) and PR [#58](https://github.com/Mnehmos/MathOS/pull/58) add the closed Rust-owned plan, task, leakage-report, and export-manifest v1 contracts; receipt-bound chronology; required declared plus derived exact relationship keys; transitive component locking; private-held-out/public-split policy; six evidence-backed task families plus conditional pedagogy tasks; explicit family skips; and database-independent deterministic reprojection after the separate platform-bound release replay. Reviewed head `2d0c8fd0ec417ea0801d8995d4b93414fcf0a814` merged as `4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`. Exact-head CI `29889101827`, merged-tree CI `29889317590`, and protected publication run `29889317589` passed.

Downloaded artifact `8517692129`, `publication-boundary-4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`, is 470,757 archive bytes with GitHub SHA-256 `5598132289fe4a6c7d5527f5dcad4129e2a1048fd3f5ea2a912d72af1902197a`; it expands to 360 files and 885,321 bytes with no links. Protected Lean 4.32 replay and independent offline verification bind source release `47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567`, canonical plan `0fe5bca2a96bff6c924cf837fa91a86b2714cf754c42cf459424f0f1d77ee9e8`, and RL export `fc0d4ccd3945aa3275a670dd5d367881c483c599bfa5350a604ed99a5ef3a5e5`. The exact 31-file export contains 30 manifest members, 102,369 member bytes, 10 private held-out tasks, one leakage component, and the six claimed families. Independent audit found zero inventory/hash/policy/trust-reference/cross-claim/cross-split/reasoning-field findings and reproduced every byte without SQLite. This completes issue #57's scoped leakage-aware foundation, but the broad SPEC 19.2/30.6 checklist criterion stays open until decomposition, proof repair, generalization, and frontier selection are projected too. Comparator, remaining pilots, migration, and full 1.0 acceptance also remain open.
Downloaded artifact `8517692129`, `publication-boundary-4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`, is 470,757 archive bytes with GitHub SHA-256 `5598132289fe4a6c7d5527f5dcad4129e2a1048fd3f5ea2a912d72af1902197a`; it expands to 360 files and 885,321 bytes with no links. Protected Lean 4.32 replay and independent offline verification bind source release `47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567`, canonical plan `0fe5bca2a96bff6c924cf837fa91a86b2714cf754c42cf459424f0f1d77ee9e8`, and RL export `fc0d4ccd3945aa3275a670dd5d367881c483c599bfa5350a604ed99a5ef3a5e5`. The exact 31-file export contains 30 manifest members, 102,369 member bytes, 10 private held-out tasks, one leakage component, and the six claimed families. Independent audit found zero inventory/hash/policy/trust-reference/cross-claim/cross-split/reasoning-field findings and reproduced every byte without SQLite. This completes issue #57's scoped leakage-aware foundation, but the broad SPEC 19.2/30.6 checklist criterion stays open until decomposition, proof repair, generalization, and frontier selection are projected too. Comparator execution, remaining pilots, migration, and full 1.0 acceptance also remain open.

Phase 6d Comparator-package work is active in issue [#60](https://github.com/Mnehmos/MathOS/issues/60). The closed plan and verification contracts project exactly the five SPEC 20.3 files, copy `Solution.lean` only from a verified frozen release, bind every staleness input and fixed repository/full-commit tool pin, and support trusted-hash offline reprojection. The local Pilot A package reprojected as `ec36212e00e255de770109a44e5bdce2e0e4922491f1a5ae950f93e6ad50ecae` from a nonexistent instance root. It is only `ready`; both verification and authority flags are structurally false. No Comparator or full verification criterion is checked until the real protected Linux sandbox runs and its exact evidence is independently audited.
Phase 6d Comparator-package issue [#60](https://github.com/Mnehmos/MathOS/issues/60) completed through PR [#61](https://github.com/Mnehmos/MathOS/pull/61). The closed plan and verification contracts project exactly the five SPEC 20.3 files, copy `Solution.lean` only from a verified frozen release, bind every staleness input and fixed repository/full-commit tool pin, and support trusted-hash offline reprojection. Reviewed head `36ae9586dc7985785501474c53e1ee3d6067b5f5` merged as `2fe5d00992599a2c22a974c01ec0cdc4fbea286d`; exact-head CI `29893380402`, merged-tree CI `29893579467`, and protected publication run `29893579466` passed.

Artifact `8519152437`, `publication-boundary-2fe5d00992599a2c22a974c01ec0cdc4fbea286d`, is 478,926 archive bytes with GitHub SHA-256 `642edf93c509407efe953a4dda588fe3190bf7bc66204d03fe1387b9a7e31384`; it expands to 373 files and 895,683 bytes with no links or reparse points. Independent audit reproduced the exact five-file, 6,095-byte package from source release `f268d9da8fa4e19a05ac32d1c85b14e9e427db326dc9a69553b1bb11d3366eff` and canonical plan `a9048a8ac02907993cd1114e3c06510524933c72b891c786d15d5beeb82c7088`. Every package/source hash and binding matched input fingerprint `aee3e4e65754205932caa8cca0937d017965bb7936d7d1cec86117e1d7225898` and verification `beef8cd5d48d9cee07352f34366db5f34c77bc73b9c685b83ded490618960758`; canonical JSON, parsed YAML, exact solution lineage, fixed tool pins, nonexistent-root reprojection, and both Lean files passed. It is only `ready`; verification and authority remain structurally false. Real protected Linux Comparator execution remains open and no full Comparator verification criterion is checked.

## Migration

Expand Down
12 changes: 7 additions & 5 deletions docs/implementation/STATUS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,11 @@ Artifact `8516235885`, `publication-boundary-e977d7eb69bfc262510c276912ba5584f35

Issue [#57](https://github.com/Mnehmos/MathOS/issues/57) completed Phase 6c through PR [#58](https://github.com/Mnehmos/MathOS/pull/58). Reviewed head `2d0c8fd0ec417ea0801d8995d4b93414fcf0a814` merged as `4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`. Exact-head CI `29889101827`, merged-tree CI `29889317590`, and protected publication run `29889317589` passed the closed RL contracts, receipt-derived temporal policy, component-level split isolation, private-held-out/public-split policy, evidence-backed task projection, explicit family skips, and offline deterministic verification after the separate release-replay gate.

Artifact `8517692129`, `publication-boundary-4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`, is 470,757 archive bytes with GitHub SHA-256 `5598132289fe4a6c7d5527f5dcad4129e2a1048fd3f5ea2a912d72af1902197a`; it expands to 360 files and 885,321 bytes with no links. Protected Lean 4.32 replay and independent offline reprojection bind source release `47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567`, canonical plan `0fe5bca2a96bff6c924cf837fa91a86b2714cf754c42cf459424f0f1d77ee9e8`, and RL export `fc0d4ccd3945aa3275a670dd5d367881c483c599bfa5350a604ed99a5ef3a5e5`. The exact 31-file export has 30 manifest members, 102,369 member bytes, 10 private held-out tasks, one leakage component, and six emitted families. Every inventory/hash/schema/source/split/temporal/reprojection check passed with a nonexistent instance root; independent audit found zero policy failures, unresolved trust-evidence references, cross-claim variants, cross-split overlaps, or forbidden reasoning fields. Decomposition, proof repair, generalization, frontier selection, Comparator, remaining pilots, migration, and full 1.0 acceptance remain open.
Artifact `8517692129`, `publication-boundary-4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`, is 470,757 archive bytes with GitHub SHA-256 `5598132289fe4a6c7d5527f5dcad4129e2a1048fd3f5ea2a912d72af1902197a`; it expands to 360 files and 885,321 bytes with no links. Protected Lean 4.32 replay and independent offline reprojection bind source release `47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567`, canonical plan `0fe5bca2a96bff6c924cf837fa91a86b2714cf754c42cf459424f0f1d77ee9e8`, and RL export `fc0d4ccd3945aa3275a670dd5d367881c483c599bfa5350a604ed99a5ef3a5e5`. The exact 31-file export has 30 manifest members, 102,369 member bytes, 10 private held-out tasks, one leakage component, and six emitted families. Every inventory/hash/schema/source/split/temporal/reprojection check passed with a nonexistent instance root; independent audit found zero policy failures, unresolved trust-evidence references, cross-claim variants, cross-split overlaps, or forbidden reasoning fields. Decomposition, proof repair, generalization, frontier selection, Comparator execution, remaining pilots, migration, and full 1.0 acceptance remain open.

Issue [#60](https://github.com/Mnehmos/MathOS/issues/60) is the active Phase 6d slice. It defines closed `comparator_package_plan/1` and `comparator_package_verification/1` contracts and projects the exact SPEC 20.3 five-file package from a frozen release. The plan supplies reviewed challenge source; `Solution.lean` is copied only from the release replay member. Release/formalization/environment/module/declaration, file, plan, input-fingerprint, and fixed repository/full-commit tool bindings are checked offline. The only encodable state is `ready` with `comparator_verified: false` and `authoritative: false`; real sandboxed Comparator execution and evidence remain a later protected transition. A Windows CLI playtest against downloaded protected release `47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567` produced and independently reprojected five-file package verification `ec36212e00e255de770109a44e5bdce2e0e4922491f1a5ae950f93e6ad50ecae` from a nonexistent instance root. Both Lean files elaborated; the challenge emitted only its intentional `sorry` warning. Exact-head and protected evidence are still required before issue closure.
Issue [#60](https://github.com/Mnehmos/MathOS/issues/60) completed the Phase 6d package boundary through PR [#61](https://github.com/Mnehmos/MathOS/pull/61). It defines closed `comparator_package_plan/1` and `comparator_package_verification/1` contracts and projects the exact SPEC 20.3 five-file package from a frozen release. The plan supplies reviewed challenge source; `Solution.lean` is copied only from the release replay member. Release/formalization/environment/module/declaration, file, plan, input-fingerprint, and fixed repository/full-commit tool bindings are checked offline. The only encodable state is `ready` with `comparator_verified: false` and `authoritative: false`; real sandboxed Comparator execution and evidence remain a later protected transition. Reviewed head `36ae9586dc7985785501474c53e1ee3d6067b5f5` merged as `2fe5d00992599a2c22a974c01ec0cdc4fbea286d`; exact-head CI `29893380402`, merged-tree CI `29893579467`, and protected publication run `29893579466` passed.

Artifact `8519152437`, `publication-boundary-2fe5d00992599a2c22a974c01ec0cdc4fbea286d`, is 478,926 archive bytes with GitHub SHA-256 `642edf93c509407efe953a4dda588fe3190bf7bc66204d03fe1387b9a7e31384`; it expands to 373 files and 895,683 bytes with no links or reparse points. Its exact five-file, 6,095-byte package binds source release `f268d9da8fa4e19a05ac32d1c85b14e9e427db326dc9a69553b1bb11d3366eff`, canonical plan `a9048a8ac02907993cd1114e3c06510524933c72b891c786d15d5beeb82c7088`, input fingerprint `aee3e4e65754205932caa8cca0937d017965bb7936d7d1cec86117e1d7225898`, and verification `beef8cd5d48d9cee07352f34366db5f34c77bc73b9c685b83ded490618960758`. Independent audit matched every package and source-member hash/size, canonical JSON and parsed YAML, the exact solution/release source, headline formalization/environment/module/declaration, and all fixed tool pins. Verification from a nonexistent instance root reproduced every byte without SQLite; both Lean files elaborated, with only the challenge's intentional `sorry` warning. The retained package remains `ready`, not Comparator-verified or authoritative.

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 @@ -246,8 +248,8 @@ These items establish only part of the product foundation and trace model. One e

## Next highest-priority criteria

1. Complete #60 review, exact-head CI, and protected artifact audit without upgrading `ready` to Comparator verification.
2. Implement the real Linux-sandboxed Comparator run and controlled evidence transition, then continue the BH Pilot C lifecycle.
1. Implement the real Linux-sandboxed Comparator run and controlled evidence transition without trusting package readiness as a result.
2. Continue the BH Pilot C lifecycle against the exact protected Comparator boundary.
3. Continue remaining pilots, migration, and section 30 criteria while preserving exact histories and negative attempts.

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

## Release readiness

Not ready. Protected Pilot A authority, fidelity, repair, pedagogy, portable-release, corpus-export, and private held-out RL/evaluation evidence exist. Comparator, remaining pilots, migration, later interfaces, and many section 30 criteria are still unfinished.
Not ready. Protected Pilot A authority, fidelity, repair, pedagogy, portable-release, corpus-export, private held-out RL/evaluation, and Comparator-ready package evidence exist. Comparator execution, remaining pilots, migration, later interfaces, and many section 30 criteria are still unfinished.
Loading
0