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

Record protected publication candidate evidence #33

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 20, 2026
Merged

Record protected publication candidate evidence #33

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
13 changes: 8 additions & 5 deletions docs/implementation/STATUS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -188,14 +188,17 @@ These items establish only part of the product foundation and Phase 2 trace mode
- PR #31 CI run `29714982064`, job `88266362527`, preserved the first hosted candidate failure: the protected rebuild and parser-derived dependency scan passed, but the axiom driver aborted while creating a Lean thread under the four-gibibyte process address-space ceiling. The repair keeps a four-gibibyte Lean heap cap, raises only the OS address-space allowance to six GiB for runtime/thread overhead, and makes future PR failures upload their bounded structured attempt evidence.
- The next PR #31 run `29715179869`, job `88266955678`, proved that the memory repair works: all three protected Lean executions passed, the dependency output contained only pinned `Init.olean`, and the axiom audit reported no axioms. It then failed closed because the producer treated a direct job snapshot as a wrapped `.job` object and attempted to copy CAS identity `null`. Failed-attempt artifact `8450312976` (`sha256:8976c4a151487bae6b414e605216fcd86c1bfe99dd792afb2cc505d0c9e145db`) retained the exact partial closure, structured executions, intermediate records, and seven CAS objects. The corrected producer now extracts and validates the direct snapshot's report, policy, and canonical-input hashes before use.
- PR #31 CI run `29715394683` passed all five required jobs on head `bf4abfe4d67dcd09ef2d717c4a706308a15676df`; its pull-request merge commit `0d14b5819ef07a733cde09a3f54c097a96f11f3b` had tree `47a28313024731861618678b80ec56d6934fa2ff`. The hosted simulated candidate completed the real canonical lifecycle, all three protected Lean executions, exact 25-member closure construction, and shared application validation. Its request, closure, and report hashes were `d38608cdf8067b14050d45e74b7c1ddb741e5b86463bc66627d8aa82b6b61bdb`, `7dad2fa6b0bc14dba31c54b38fabaec5cd9bcaa812aa2d7877c6586380fa8cd5`, and `0bb66bee9114141efe9ae6202fe9b3931f88e460d1262d6df5cb82154eba8278`; the validation result remained `authoritative:false`.
- PR #31 merged as commit `55a0ae0fad9fe5cfd20ed0a5fbddf6b80a5303c1`, tree `7508582f4ac01b6cd4533c135d7da5f238ad2149`; main CI run `29716292647` passed all five jobs. The first protected candidate run `29716292659` passed the protected-ref gate, smoke execution, smoke attestation, and constrained smoke challenge, then failed closed with exit `65` because the script's report-vocabulary constant `RUNNER_ENVIRONMENT=github_hosted` shadowed GitHub's immutable `RUNNER_ENVIRONMENT=github-hosted`. Failed artifact `8450708477` retained the completed smoke evidence with archive digest `29c70446a4ba089b44621b254bd6ff54ca3a109a836ff8c60a4525e8e7059c27`.
- PR #32 renamed only that internal constant and merged as `fc9116492a60fd891bbb1a175096002c8ab504a4`, tree `5dc109a29888c7ac34e67cdd6fb84454947133e5`. Main CI run `29716676603` passed all five jobs. Protected publication run `29716676599`, job `88271222144`, then completed candidate construction, attestation, independent challenge, and unconditional retention. Artifact `8450846116` has GitHub archive digest `1e0ecbf1ca9250494e164ffe8fe093e4b2a99ca4aa34bcaa1126c9a698ff26e6`.
- Downloaded inspection of that first exact protected candidate verified all 25 sorted fixed-path roles and every member byte hash. The canonical request, retained closure, publication report, retained validator result, and attempt summary hashes are `9f32d3eca940100b92f6ceb91e975fb859f99c1cf97fb98ae859e6cd79419103`, `ff67bc6f101681ff5c8345c763036ca1c07caed4eec714ba8c35f5017a5c28e3`, `12f0aaca0f6e9a16c242205da24f53fadc08ba9177cff6e039ec394c50ee1012`, `1d5adfc932ffa566f859c45caba62d97443e80ee1a3eb4532f792e5ca69362c0`, and `503c86845b6e0a78fa3712b9cf999f78203c15df2550356e3965a12944740ea5`.
- Inspection also confirmed exact source commit, tree, run, and attempt binding; clean checkout; empty declared imports; only pinned `/opt/lib/lean/Init.olean` in protected dependency output; no axioms in both local and protected audits; seven intact retained CAS objects; and passed rebuild, dependency, and axiom execution records. The candidate Sigstore bundle, raw pinned-`gh` verification, and constrained verification-record hashes are `a23d190fdaffe7e87fc98747b32525f96f199aa05f5431cba39548b38207a84e`, `1e6063a8ca1ef58476992d8691f702cc39d547ce94d82ebf90a848eef75d549a`, and `93871363affcfcc6a36d954577779de5791752d2951340c90f77df095c81ce3a`. The certificate binds the exact protected workflow, `main`, merge commit, push event, and GitHub-hosted runner; its subject matches the report and its verified Rekor timestamp is `2026-07-20T04:22:41Z`. Every candidate, attempt, validation, and verification record remains `authoritative:false`.

## Next highest-priority criteria

1. Download and inspect the first exact merged protected candidate artifact, then record its report, closure, bundle, raw-verifier, and constrained-record identities.
2. Implement controlled application ingestion that revalidates the downloaded closure and attestation before creating any authority.
3. Create authoritative exact proof/refutation evidence only from that verified retained closure, never from caller-authored reports.
4. Derive mathematical status only from exact current proof and fidelity evidence.
5. Complete Pilot A through the real interfaces only after both authority and fidelity controls exist.
1. Implement contro 5BF2 lled application ingestion that revalidates the downloaded closure and attestation before creating any authority.
2. Create authoritative exact proof/refutation evidence only from that verified retained closure, never from caller-authored reports.
3. Derive mathematical status only from exact current proof and fidelity evidence.
4. Complete Pilot A through the real interfaces only after both authority and fidelity controls exist.

## Exact last validation commands

Expand Down
Loading
0