Repository navigation
Phase 6g: bind source records to verified portable content for Pilot C #71
Description
Goal
Make a canonical source/1 content hash mean what it says before beginning the BH Pilot C lifecycle: when source content is retained, the exact artifact must exist, rehash from CAS, remain policy-compatible, and travel in every portable release that contains the source record.
This is a focused prerequisite for SPEC 29.3(1) and 29.3(9). It creates no mathematical, fidelity, definition, reuse, coverage, kernel, or Comparator authority.
Exact discovery evidence
Canonical MathOS main at discovery:
- commit
348f9abe8f74df053bce76ed90b34df41abace02 - tree
8eeb521e6e10e76c39008ab5aa6882a6552ef3ec
Pinned Pilot C repository source inspected through gh:
- repository
Mnehmos/BHFormalization - commit
8875bef812375d7e6fd00bff95764cd5c057c7fe - tree
600f3e1230ca88f9784837933e2417c319aaad3e - release
v1.0.0 - licensed Lean formalization: Apache-2.0
- exact source-lock artifact SHA-256
c82096766a9df350fc2584cdabd0e18334348a1a8adbd4fc7ec24d75ff2994ee
A real Windows CLI playtest ingested that source-lock artifact and created repository source 019f9b03-c8dc-7620-921c-b01acb95ff29@cb1a1aded792ae97d94f3054a2d3a06120b183aed3c38d83bb905982eb23d6a7. A negative dry-run then accepted nonexistent content hash 0000…0000 and proposed version 5172f12dc1f72036cd669bd09787c90722a2557760d0956886dfcaeec7aafd49. No invalid record was persisted.
The portable release builder currently closes formalization and learning-unit artifacts but not SourcePayload.content_hash, so a release can carry a content-hashed source record without its claimed source bytes.
Compatibility and trust decisions
- Keep
source/1canonical bytes and version-hash semantics unchanged. - Keep
content_hash: nullvalid where content is deliberately not retained; do not invent bytes or licensing authority. - When
content_hashis present, it is a real exact CAS reference, not caller-authored metadata. - Existing mathematical authority and fidelity paths remain separate and unchanged.
- BH paper, upstream reproducibility bundle, and Apache-licensed Lean formalization remain distinct sources with distinct licenses and provenance. This slice must not conflate the paper certificate with the separately generated Lean certificate.
- Issues Replace single verified status with multidimensional trust and promotion states #67, Add source-grounded definition policy and immutable definition review gates #68, and Add collaboration-first upstream contribution workflow for established Lean libraries #69 remain open. This content-closure work must not silently mark definitions grounded, artifacts reusable, theorem coverage complete, or an upstream contribution approved.
Deliverables
- Application validation shared by CLI and MCP for source create/version, dry-run, persistence, and exact retry:
- resolve every non-null source content hash to registered artifact metadata;
- reread and rehash exact CAS bytes;
- require reviewed
source_contentsemantic role; - reject absent, corrupt, unsafe, or policy-incompatible content;
- recheck dependencies at the mutation boundary.
- Portable release construction includes every retained source-content artifact in the exact closure.
- Database-independent release verification independently requires and rehashes each source-content member.
- Public export remains fail-closed on unresolved/restricted licensing; private retention preserves the original restriction.
- A small Apache-2.0 BH repository fixture pinned to the exact commit/tree above exercises real source ingestion without claiming paper correspondence.
- Documentation records the source-content trust boundary and Pilot C remains incomplete.
Acceptance criteria
- A missing all-zero or unregistered source content hash fails in dry-run and persisted create/version through CLI and MCP.
- Wrong ro 8000 le, changed metadata, missing CAS, changed bytes, unsafe path, license escalation, and redaction/redistribution mismatch fail closed.
- Exact create/version retries are deterministic and cannot conceal damaged source content.
- Existing
content_hash: nullrecords and canonicalsource/1hashes remain byte-compatible. - A release containing a content-hashed source contains the exact artifact once, with matching hash/size/license/restriction.
- Offline verification with SQLite absent passes the untouched bundle and rejects missing, altered, substituted, or extra source bytes.
- The pinned BH source-lock fixture ingests and retrieves byte-identically through the real CLI; its missing-hash negative probe fails.
- Formatting, warnings-denied Clippy, all Rust/CLI/MCP/Lean/Python gates, exact-head CI, merged-main CI, and protected playtest pass before closure.
Non-goals
- Claiming the BH paper and Lean theorem are faithful equivalents.
- Importing or verifying the full BH proof/certificate in this slice.
- Implementing the full multidimensional trust model, definition approval, or upstream collaboration workflow.
- Completing Pilot C or MathOS 1.0.
Activity
Mnehmos commentedon Jul 25, 2026
Implementation is in PR #72 at commit
d1548fae8b60b6161123c03be7455f4b8e1bc942(treec680ecd732e2318d94e02485197b541b96fd91de).Provenance correction from the implementation audit: the discovery SHA-256
c82096766a9df350fc2584cdabd0e18334348a1a8adbd4fc7ec24d75ff2994eeis the 1,848-byte CRLF rendering produced by the Windows checkout. A directgh apiread ofBHFormalization/SOURCE-LOCK.mdat pinned commit8875bef812375d7e6fd00bff95764cd5c057c7fereturns the canonical 1,809-byte Git blobc7e3805ab78327f1cd561421e2c0168a009eb161, whose SHA-256 is249f62a4e2780235239cf9f4e781f274f8dadba7f3aeba3aab51f46b0a6fc5c5. The committed fixture, CLI assertions, release assertions, and documentation use that platform-independent Git-object identity.Mnehmos commentedon Jul 25, 2026
Phase 6g is complete through PR #72.
Exact implementation and merge:
433ec5895076523525305263505451362b7ca5e4a208205686e88ccb9cabf79b730680b0a159727c2adcae8e69028a29f67911aa5dd4903f4efaf9e530176105648: success on Ubuntu Rust, Windows Rust, real storage, pinned Lean, and legacy Python30176242832: success30176242820: success89725373077: success89725548018: successProtected retained evidence:
8624303951, Actions digestsha256:eeb5a5c6452d9a1a1589e63e24f98543b56a4c1571422acc6b0c0e2e9078461e8624380298, Actions digestsha256:1f1f22fcafbe5df275f557d220e4bd7780072badb46b332afc5329b971712a75da2524133f42741bf0ce6c62d9f27f50885c25e6f52b4a2c877bd318bc07c2f9An independent audit of the downloaded publication-boundary artifact checked all 83 manifest members (84 files including the manifest), every declared byte size and SHA-256, exact inventory equality, zero links/reparse points, and zero database files. The dry-run, build, and offline-verification manifest hashes are identical; the retained playtest records
database_hidden_during_verification: true, clean-copy verification, Lean replay, and Comparator reprojection success.The protected release contains one non-null source binding,
019f9b3e-ce4e-7b30-bc83-49e317e2ed45@e5afe48aeb0566471a845b9c3efce146a7703b9505f94d39a8e20928cd468190. Its exact artifact occurs once atartifacts/aa1476702fa9b4b66c8fa04048a1282e7fc035704f64424ca2a2bd998b13dee1, is 1,421 bytes, private,user_ingest, license-null, and carriessemantic_metadata.source_role = source_content. A directgh apiread of the merged fixture returns Git blob8b6e382c98233cc26d0b95a2a98ac313b7bf68e0, the same 1,421 bytes and SHA-256; the released artifact is byte-identical.The BH conformance fixture is separately pinned to upstream Git blob
c7e3805ab78327f1cd561421e2c0168a009eb161(1,809 bytes), SHA-256249f62a4e2780235239cf9f4e781f274f8dadba7f3aeba3aab51f46b0a6fc5c5. The issue's discovery digestc8209676...was correctly identified and documented as a CRLF Windows worktree rendering, not the portable Git-object identity.Acceptance is satisfied across CLI and MCP dry-run/persisted create/version rejection, exact create/version retry damage checks, null compatibility, SQL/migration defense, Windows junction rejection, one-member portable closure, database-free verification, full local gates, exact-head CI, merged-main CI, and the protected playtest.
This closes source-content integrity and portability only. It creates no paper correspondence, fidelity, definition, reuse, coverage, Lean-kernel, Comparator, mathematical-status, or contribution authority. Pilot C remains incomplete; #67, #68, and #69 remain open.