8000 Record Comparator authority audit evidence by Mnehmos · Pull Request #70 · Mnehmos/MathOS · GitHub
[go: up one dir, main page]

Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
3 changes: 3 additions & 0 deletions .gitattributes
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
# Shell entry points must remain executable as LF-delimited scripts on every checkout.
*.sh text eol=lf

# The protected Comparator report binds this probe's exact invocation-file digest.
scripts/comparator-network-probe.py text eol=lf

# These vendored files are cryptographic inputs and must retain their upstream bytes.
schemas/mathcorpus/upstream-*/* -text
schemas/mcip/v1/upstream-*/* -text
Expand Down
2 changes: 1 addition & 1 deletion docs/implementation/RELEASE_CHECKLIST.md
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ Artifact `8519152437`, `publication-boundary-2fe5d00992599a2c22a974c01ec0cdc4fbe

Phase 6e Comparator-execution issue [#63](https://github.com/Mnehmos/MathOS/issues/63) completed through PR [#64](https://github.com/Mnehmos/MathOS/pull/64), merge `3a75ddc8bc5de685dc6425d6158791553be0ca40`. Exact-head CI `29898468563`, merged-tree CI `29898749801`, and protected publication run `29898749807` passed. Downloaded artifact `8521103391` independently verified the exact 20-file official run bundle without SQLite: report `42b29ecd69b222c26e1de47bed83f6e3e8df5910f35f1c2543a2d9ed72eb3198`, package verification `7a3adfa8e30085cbda8ca240ab8288909a088d7ae0f9880ba0cc5b410645cc52`, attestation bundle `a447696ceeb6e537c0bc6e5ebf81ab95d2e91006df57aa2bb632edc60d4cf0a5`, and artifact digest `sha256:f322f92281ea6cc70f70cdc657d32a2029f559328be50c434ef857e4714403ba`. The accepted report proves the scoped official execution boundary only and remains `authoritative: false`.

Phase 6f issue [#65](https://github.com/Mnehmos/MathOS/issues/65) has an implementation candidate for the separate authority transition: byte-compatible evidence v1/v2 plus closed `evidence/3`, exact CAS staging and reprojection, pinned constrained attestation receipt, receipt-only derived promotion, immutable Store and SQL defenses, live current/stale replay, and one CLI/MCP application path. Comparator evidence is deliberately excluded from Lean proof/refutation claim-status inputs. The scoped checklist evidence remains provisional until exact-head CI, a protected same-run promotion, and an independent database-free retained-artifact audit pass.
Phase 6f issue [#65](https://github.com/Mnehmos/MathOS/issues/65) completed through PR [#66](https://github.com/Mnehmos/MathOS/pull/66), merge `3e199a847a27202bfdf04db8384ebf930c275325`, tree `940f0f6e2cb0abe1c4bfcace607eab2235ec6414`. Exact-head CI `30172477751`, merged-tree CI `30172614043`, and protected publication `30172614051` passed. Downloaded artifact `8623423197` has Actions digest `sha256:824949af9590d58a3c7e39eaa25edac3d2779b9d3650b984332884b584172a26`; an independent database-free audit checked all 139 files, 91 portable objects, 104 staged artifacts, exact retry bytes, and every authority/provenance/currentness binding with no links or database files. Stage `b4c84618c1266186a58bd69adf161f6234563b98af01dd5d31aab6a43eb8179e` produced receipt `5f4b8c61134728c0e35b653ae17c7a3075f52bbfeff2b6fe7c5435845ae7a0cc` and current authoritative evidence `019f9ae3-4217-7591-897a-fc97d7188a34@349684d71dc51ee1c526c533ae661daee44c09b61419ac441d1474776fd0bfeb`. Report `1fa186aab178215280e63675d36c4be497106db238f70f9cf09489edd2c04233`, package verification `f8587103c57136ede329d8bde4ab268f3ca9e7fb0596d01d40bdb14989637e23`, release manifest `e93c8644f4053645b888f3347c45bc8757ace33660c8fa1b2fea75796eb65beb`, attestation bundle `28a7294ff0aafe89bc0ef75c1d87d7b532d1c4458d6a9caa017c13fd1cc68e12`, and raw verification `81bd23fc9262d36a1a781320e5c8b08e8769914596543d9f278af8b9ae997cf8` replay exactly. Report and receipt stay non-authoritative; Comparator authority remains excluded from Lean proof/refutation claim status.

## Migration

Expand Down
17 changes: 9 additions & 8 deletions docs/implementation/STATUS.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Implementation Status

Last updated: 2026-07-22
Last updated: 2026-07-25

## Release truth

Expand Down Expand Up @@ -38,7 +38,9 @@ Issue [#63](https://github.com/Mnehmos/MathOS/issues/63) completed the Phase 6e

Artifact `8521103391`, `comparator-run-3a75ddc8bc5de685dc6425d6158791553be0ca40`, has Actions archive digest `sha256:f322f92281ea6cc70f70cdc657d32a2029f559328be50c434ef857e4714403ba`. Independent offline audit verified the exact 20-file bundle without SQLite or reparse points. Canonical report `42b29ecd69b222c26e1de47bed83f6e3e8df5910f35f1c2543a2d9ed72eb3198` accepted package verification `7a3adfa8e30085cbda8ca240ab8288909a088d7ae0f9880ba0cc5b410645cc52`; its attestation bundle is `a447696ceeb6e537c0bc6e5ebf81ab95d2e91006df57aa2bb632edc60d4cf0a5`. The official run exited zero with bounded 900-byte stdout, empty stderr, seven ordered unique success markers, UID 1001, strict Landlock ABI 5, `NoNewPrivileges=yes`, and active AF_UNIX and loopback TCP denial. The report remains structurally `authoritative: false`.

Issue [#65](https://github.com/Mnehmos/MathOS/issues/65) is the active Phase 6f authority slice. Its implementation candidate preserves `evidence/1` and `evidence/2` bytes and adds a closed `evidence/3` `comparator_run` contract, immutable non-authoritative stage and attestation-receipt records, a committed policy pin, receipt-only promotion, live current/stale replay, independent Store/SQL/read-time gates, and CLI/MCP parity. The protected workflow now transfers only the canonical state needed by the separate Comparator job and is designed to retain a database-independent content-addressed authority closure. Exact-head CI, protected execution of the new gate, and independent downloaded-artifact audit are still required before #65 can close; no authoritative Comparator evidence is claimed yet.
Issue [#65](https://github.com/Mnehmos/MathOS/issues/65) completed the Phase 6f authority slice through PR [#66](https://github.com/Mnehmos/MathOS/pull/66). Reviewed head `4422168c81178b10b5b06f3b60f88af7ec3bcfb5` merged as `3e199a847a27202bfdf04db8384ebf930c275325`, tree `940f0f6e2cb0abe1c4bfcace607eab2235ec6414`. Exact-head CI `30172477751`, merged-tree CI `30172614043`, and protected publication run `30172614051` passed. The implementation preserves `evidence/1` and `evidence/2` bytes and adds a closed `evidence/3` `comparator_run` contract, immutable non-authoritative stage and attestation-receipt records, a committed policy pin, receipt-only promotion, live current/stale replay, independent Store/SQL/read-time gates, and CLI/MCP parity.
Comment thread
Mnehmos marked this conversation as resolved.
Resolved

Downloaded artifact `8623423197`, `comparator-run-3e199a847a27202bfdf04db8384ebf930c275325`, has Actions archive digest `sha256:824949af9590d58a3c7e39eaa25edac3d2779b9d3650b984332884b584172a26`. Independent database-free audit checked all 139 files, 91 portable CAS objects, 104 staged artifacts, the exact 20-file run and 84-file release, zero links/reparse points, zero database files, canonical bytes, retry stability, and every retained binding. Stage `b4c84618c1266186a58bd69adf161f6234563b98af01dd5d31aab6a43eb8179e` produced receipt `5f4b8c61134728c0e35b653ae17c7a3075f52bbfeff2b6fe7c5435845ae7a0cc` and authoritative Comparator evidence `019f9ae3-4217-7591-897a-fc97d7188a34@349684d71dc51ee1c526c533ae661daee44c09b61419ac441d1474776fd0bfeb`. Live replay is `current` and `authoritative: true`; its exact report `1fa186aab178215280e63675d36c4be497106db238f70f9cf09489edd2c04233`, package verification `f8587103c57136ede329d8bde4ab268f3ca9e7fb0596d01d40bdb14989637e23`, release manifest `e93c8644f4053645b888f3347c45bc8757ace33660c8fa1b2fea75796eb65beb`, attestation bundle `28a7294ff0aafe89bc0ef75c1d87d7b532d1c4458d6a9caa017c13fd1cc68e12`, and raw verification `81bd23fc9262d36a1a781320e5c8b08e8769914596543d9f278af8b9ae997cf8` all replay exactly. The report and receipt remain structurally non-authoritative, and Comparator evidence remains excluded from proof/refutation claim-status inputs. The exact protected probe is now LF-pinned across Windows checkouts because its digest is part of the invocation binding.

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

## Next highest-priority criteria

1. Complete issue #65 exact-head CI, protected receipt-bound promotion, and independent portable-artifact audit without trusting package or report fields.
2. Continue the BH Pilot C lifecycle against the resulting exact protected Comparator authority boundary.
3. Continue remaining pilots, migration, and section 30 criteria while preserving exact histories and negative attempts.
1. Continue the BH Pilot C lifecycle against the exact protected Comparator authority boundary completed in issue #65.
2. Continue remaining pilots, migration, and section 30 criteria while preserving exact histories and negative attempts.

## Exact last validation commands

Expand All @@ -278,9 +279,9 @@ git diff --check
Observed validation evidence for this update:

- Home workstation: Windows 10.0.19045, PowerShell 5.1.19041.6456, Rust 1.97.1, Python 3.12.10, GitHub CLI 2.70.0, GNU Bash 5.2.37 through Git for Windows, and Lean 4.32.0 `x86_64-w64-windows-gnu`.
- Formatting, warnings-denied Clippy across all targets and features, 187 library tests, 20 CLI tests, four MCP tests, the opt-in real Lean 4.32 lifecycle, all 39 legacy Python regressions, Bash syntax and ShellCheck 0.11.0 for the Comparator authority script, Actionlint 1.7.12, and patch whitespace validation pass for the Phase 6f implementation candidate.
- Formatting, warnings-denied Clippy across all targets and features, 187 library tests, 20 CLI tests, four MCP tests, the opt-in real Lean 4.32 lifecycle, all 39 legacy Python regressions, Bash syntax and ShellCheck 0.11.0 for the Comparator authority script, Actionlint 1.7.12, and patch whitespace validation passed for the Phase 6f implementation.
- Comparator-specific local coverage preserves the committed evidence v1/v2 schemas and identities, matches every new committed schema and the policy hash, parses the exact protected Pilot A report/bundle/verifier fixture, applies migration 12 idempotently, and passes four Store authority tests covering exact retry, receipt uniqueness, immutable stage/receipt rows, direct-SQL closure/policy rejection, claim-status noninterference, current-head conflict, and read-time projection tampering. CLI and MCP tests expose the same four application actions, reject filesystem escape and caller-authored authority selectors, and fail closed for missing stages and receipts.
- The new protected-main step is locally syntax- and workflow-valid but has not run on protected `main`. No Phase 6f receipt, `evidence/3` identity, currentness result, or portable retained-artifact hash is recorded until the implementation merges and that artifact is independently audited.
- The protected-main Phase 6f step passed in run `30172614051`. Independent audit of retained artifact `8623423197` verified the database-free stage, receipt, `evidence/3` identity, complete portable closure, and live `current` result recorded above.
- The retained Pilot A release proj 6736 ected twice to manifest `33e6ccc24979e85c14688d755130ace9960f0e074342695e951ac9756c2c590b` with 11 members and 101,695 bytes. Verification from a nonexistent instance root independently reprojected the exact source release and passed every inventory, hash, schema, policy, and binding check. The pinned upstream `validate_packets.py --check-hashes --warn-as-error` and `validate_mcip.py --check-hashes` commands reported zero errors and zero warnings.
- The application-level authority fixture constructs the real source/claim/formalization, diagnostic and audit jobs/evidence, exact 25-role retained closure, parser-valid protected attestation output, stage, and receipt without fidelity evidence. Dry-run writes no evidence; persisted promotion creates the expected receipt-bound authoritative `evidence/2`; exact retry is identical; and missing staged CAS fails closed. A hands-on Windows CLI smoke applied migration 11, reported healthy `mcl health` and `mcl doctor`, exposed only the receipt-hash promotion surface, and rejected an unknown receipt as `MCL_PUBLICATION_RECEIPT_NOT_FOUND`.
- CodeRabbit's final review found one uncovered fail-closed test family. Commit `761171fb093cecc4b2391ac53ef89c315ff1eeea` now tests rejected/failed classifications, each required protected-report control independently set false while classification remains passed, and a pre-authoritative report. Formatting, full Rust tests, warnings-denied Clippy, and all five required PR jobs passed on that exact head.
Expand All @@ -306,4 +307,4 @@ Observed validation evidence for this update:

## Release readiness

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