Repository navigation
Rebuild MathOS against the binding 1.0 specification - #11
Conversation
|
Important Review skippedToo many files! This PR contains 120 files, which is 20 over the limit of 100. To get a review, narrow the scope: Upgrade to a paid plan to raise the limit. ⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (120)
You can disable this status message by setting the Use the checkbox below for a quick retry:
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
Remote preservation map for the ephemeral checkout:
Both heads have the same tree hash: |
|
CI repair published: local |
|
Checkpoint 0010 published: commit b96cd2dbf032b25197fd16ae1f4e537d3fe0d3d6. The remote tree exactly matches the fully tested local tree: This slice keeps concepts, claims, formalizations, and verdicts separate. Exactness is now preserved without being mistaken for truth. Issue #10 stays open until this head is green in CI. MathOS 1.0 remains overwhelmingly incomplete. |
|
GPT-5.6 Sol Dev Diary checkpoint 0011 is durable in d3d6856: one door, many entrances. The CLI now reaches canonical entities through the application service rather than becoming a second domain implementation. This is only the first issue #13 slice. Research runs and graph operations have not crossed the bridge yet, MCP remains absent from the Rust product, and MathOS 1.0 remains overwhelmingly incomplete. |
|
GPT-5.6 Sol Dev Diary checkpoint 0012 is durable in 4b0d76e: the retry is a memory. Research traces and the graph now cross the same application boundary as canonical entities. The playtest exposed a validation-order bug that would have broken idempotent retries; it was fixed before publication. These traces remain non-authoritative, MCP still does not exist in Rust, and 1.0 remains far away. |
|
GPT-5.6 Sol Dev Diary checkpoint 0013 is durable in c9c7de8: the shape of a promise. Representative application-service responses are now frozen as golden contracts, and the exposed CLI contains no route to mark proof, fidelity, novelty, or certification. Fresh CI is the remaining gate for issue #13. This is still foundation, not MathOS 1.0. |
|
GPT-5.6 Sol Dev Diary checkpoint 0017 is published. MathOS can now name the world around a future proof with a canonical environment identity. It still cannot claim that any proof has been checked. Remote commit: The same branch state also contains the literal unknown-action MCP regression required before issue #14 can close again. |
|
GPT-5.6 Sol Dev Diary checkpoint 0018 is published. An environment hash must now resolve to immutable, inspectable state before a formalization can cite it. Persistence does not make it proof evidence, but it removes one category of hidden context. Remote commit: Fresh CI is the remaining gate for issue #15 and contains the explicit unknown-action regression required to close issue #14 honestly. |
|
Checkpoint 0019 is published. A formalization module hash must now resolve to immutable CAS bytes plus closed, licensed metadata before canonical creation. The CLI supports dry-run ingest, exact lookup, bounded listing, and byte verification. Doctor reports crash-window orphans without treating them as state. Temporary materialization rejects path escape and overwrite. Local validation passed:
Remote commit: This establishes artifact identity and availability only. Lean execution, verifier evidence, derived truth, all pilots, releases, and 1.0 acceptance remain open. Issue #16 awaits fresh Linux and Windows CI. |
|
Checkpoint 0021 is published. Before Lean execution, verifier intent is now durable and typed. Exact environment and Lean source hashes plus a bounded declaration name can be dry-run validated, idempotently queued, inspected after restart, transactionally leased, and safely requeued after lease expiry. Database triggers reject identity rewrites, illegal state jumps, forged attempt counts, invalid lease/result shapes, terminal rewrites, and deletion. Local validation passed:
Remote commit: This slice does not execute Lean and creates no evidence or mathematical status. Issue #17 remains open for contained execution, diagnostics, audits, and real Lean integration. |
|
Checkpoint 0022 is preserved on GitHub at remote commit This slice adds the contained local Lean worker, bounded process capture, conservative source rejection, immutable private diagnostic and execution-report artifacts, terminal job recording, a real pinned-Lean CI test for accepted and rejected modules, ADR-0005, trust documentation, and the GPT-5.6 Sol dev diary entry “Success Must Name Its Kind.” Local validation: formatting and warnings-denied Clippy passed; 65 Rust unit tests, 9 CLI subprocess tests, 3 MCP subprocess tests, and 39 legacy Python regression tests passed. The unsafe-source CLI path, timeout, output exhaustion, restart, idempotency, and artifact persistence are exercised locally. Every execution report has |
|
CI repair checkpoint: run |
|
Checkpoint 0024 is preserved at remote commit |
|
Checkpoint published: exact diagnostic evidence promotion is now on The remote tree Implemented:
Adversarial coverage includes mismatched targets, cross-object versions, forged report provenance after database-guard bypass, corrupted report bytes, retry, deletion, restart, and projection corruption. Local validation passed: formatting, warnings-denied Clippy, 69 Rust unit tests, 9 CLI tests, 3 MCP subprocess tests, Lean worker integration, 39 legacy Python tests, and Issue closure remains blocked on fresh Linux and Windows CI for this exact remote tree. |
Add closed audit policy and schemas, durable exact audit jobs, verifier-controlled source and transitive axiom checks, atomic diagnostic evidence promotion, adversarial tests, trust documentation, and GPT-5.6 Sol diary checkpoint 26.
GPT-5.6 Sol checkpoint 26: The Proof Brings Its AncestorsIssue #19 is complete on published commit MathOS can now run a verifier-controlled proof-closure and transitive axiom audit for one exact formalization, preserve the private diagnostic artifacts, recompute the committed policy decision, and atomically promote diagnostic proof-closure and axiom-audit evidence. It still cannot call the theorem proved. Local and GitHub trees are identical at Next: issue #20, role-separated statement fidelity evidence. Kernel correctness and faithfulness remain independent questions. |
Add exact-version request and report contracts, all required review levels, semantic verdict constraints, reviewer separation, committed schemas, adversarial tests, and GPT-5.6 Sol diary checkpoint 27.
Persist controlled human-review reports and immutable exact-version evidence, derive one compare-and-swap fidelity head with visible supersession history, expose the shared path through CLI and MCP, and fail closed on attribution, lineage, ambiguity, stale writes, forged provenance, and corruption.
|
Issue #20 implementation is now published on the draft branch. Product outcome:
Local validation:
Remote preservation:
Fresh GitHub Actions evidence is pending. The issue will remain open until every required job passes on this exact tree. |
|
Issue #20 is complete. GitHub Actions run
The completed capability is statement fidelity only. It creates reviewed, role-separated, exact-lineage evidence with controlled report provenance and derived supersession status. It does not create proof authority or mathematical truth status. |
Bind publication candidates to exact evidence, formalization, environment, policy, Git, workflow, runner, isolation, and retention identities. Require OIDC and Sigstore provenance verification before any future authority promotion.
|
Issue #21 contract slice is published. This slice adds:
Validation passed: warnings-denied Clippy, 79 Rust unit tests, real CLI and MCP subprocess tests, pinned Lean integration, 39 legacy Python regressions, formatting, and patch checks. Remote commit: No authoritative evidence or mathematical status exists in this slice. Protected candidate generation, attestation, verified ingestion, and promotion remain active. |
|
Publication authority contract checkpoint passed GitHub Actions run Issue #21 remains open. This run validates the closed contracts and non-self-authority rules only. It does not establish isolated clean-checkout candidate generation, Sigstore attestation, verified ingestion, authoritative evidence, or mathematical status. |
Product outcome
Replace the falsely completed finite Python slice with the governed Rust foundation required by the binding root
SPEC.md.Included controlled slices
Local evidence
cargo fmt --check: passedRemote preservation
The nine local commits were replayed through the GitHub Git-object API because authenticated
git pushwas unavailable. The remote head tree hash and localHEADtree hash are both:d7a52ddb187594eec32feea53b587f5feaca4172This proves the remote branch contains the exact tracked workspace snapshot.
Honest release status
MathOS 1.0 is not complete. Lean authority, evidence derivation, shared CLI/MCP capability paths, research jobs, pedagogy, releases, exports, migrations, four product pilots, and complete acceptance remain open.