Repository navigation
Pilot A: prove the repaired claim through the protected boundary - #47
Merged
Merged
Conversation
📝 WalkthroughWalkthroughThe PR adds a repaired Pilot A theorem and extends publication scripts and workflows to support separate refutation and repaired-proof candidates, shared canonical state, retained artifacts, protected ingestion, CI validation, and updated implementation and authority documentation. ChangesPilot A repaired publication
Estimated code review effort: 4 (Complex) | ~45 minutes Sequence Diagram(s)sequenceDiagram
participant ProtectedWorkflow
participant publication_candidate as publication-candidate.sh
participant publication_ingest as publication-ingest.sh
participant MCL
ProtectedWorkflow->>publication_candidate: build refutation candidate
publication_candidate->>MCL: create and attest refutation evidence
ProtectedWorkflow->>publication_ingest: ingest and repair refutation candidate
publication_ingest->>MCL: retain repaired claim and repair lineage
ProtectedWorkflow->>publication_candidate: build repaired-proof candidate
publication_candidate->>MCL: formalize and attest repaired proof
ProtectedWorkflow->>publication_ingest: ingest repaired-proof candidate
publication_ingest->>MCL: verify proof authority and separated evidence
Possibly related issues
Possibly related PRs
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 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 |
7 tasks done
Mnehmos
marked this pull request as ready for review
July 21, 2026 21:25
Owner
Author
|
@codex review |
There was a problem hiding this comment.
Actionable comments posted: 1
🧹 Nitpick comments (2)
.github/workflows/publication.yml (2)
20-20: 🩺 Stability & Availability | 🔵 TrivialTimeout bump may be tight for two sequential closures.
This job now runs two full protected candidate closures (original + repaired-proof) plus two ingestions and two attestation verifications sequentially. A 5-minute bump (15→20) may be insufficient if a single closure already takes a meaningful fraction of that budget; worth confirming against observed run times.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In @.github/workflows/publication.yml at line 20, Reassess the timeout-minutes setting for the publication job to account for two sequential protected candidate closures, ingestions, and attestation verifications. Use observed workflow runtimes to select a timeout with sufficient headroom rather than retaining the potentially tight 20-minute limit.
99-159: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winDuplicate env blocks for the two candidate closures.
The env block for the original candidate build (Lines 101-110) is duplicated verbatim for the repaired-proof candidate build (Lines 143-151). Hoisting these shared publication context vars to job-level
env:would remove the duplication and eliminate the risk of the two closures silently drifting apart if one block is edited without the other.♻️ Proposed refactor: hoist shared env to job level
boundary: name: Attested publication candidate boundary if: github.ref == 'refs/heads/main' runs-on: ubuntu-latest timeout-minutes: 20 + env: + PUBLICATION_CONTEXT_MODE: protected-main + PUBLICATION_REPOSITORY: ${{ github.repository }} + PUBLICATION_WORKFLOW_PATH: .github/workflows/publication.yml + PUBLICATION_WORKFLOW_REF: ${{ github.workflow_ref }} + PUBLICATION_SOURCE_REF: ${{ github.ref }} + PUBLICATION_SOURCE_COMMIT_SHA: ${{ github.sha }} + PUBLICATION_WORKFLOW_RUN_ID: ${{ github.run_id }} + PUBLICATION_WORKFLOW_RUN_ATTEMPT: ${{ github.run_attempt }} + PUBLICATION_RUNNER_ENVIRONMENT: github_hosted permissions: contents: read ... - name: Build and validate the exact protected candidate closure shell: bash - env: - PUBLICATION_CONTEXT_MODE: protected-main - ... run: | ... - name: Build and validate the repaired claim proof in canonical state shell: bash - env: - PUBLICATION_CONTEXT_MODE: protected-main - ... run: | ...🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In @.github/workflows/publication.yml around lines 99 - 159, Hoist the shared PUBLICATION_* context variables currently repeated in the “Build and validate the exact protected candidate closure” and “Build and validate the repaired claim proof in canonical state” steps into the job-level env configuration. Remove both step-level duplicate env blocks while preserving the existing step-specific shell commands and variable values.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/trust/PUBLICATION_AUTHORITY.md`:
- Around line 63-65: Update the “Current implementation state” section to
include the repaired-proof candidate’s publication flow, proof authority,
claim-relation fidelity evidence, and derived proved status. Align it with the
implemented behavior described in the protected workflow, removing any wording
that presents repaired-proof publication as absent while preserving the existing
refutation and counterexample-repair details.
---
Nitpick comments:
In @.github/workflows/publication.yml:
- Line 20: Reassess the timeout-minutes setting for the publication job to
account for two sequential protected candidate closures, ingestions, and
attestation verifications. Use observed workflow runtimes to select a timeout
with sufficient headroom rather than retaining the potentially tight 20-minute
limit.
- Around line 99-159: Hoist the shared PUBLICATION_* context variables currently
repeated in the “Build and validate the exact protected candidate closure” and
“Build and validate the repaired claim proof in canonical state” steps into the
job-level env configuration. Remove both step-level duplicate env blocks while
preserving the existing step-specific shell commands and variable values.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 2ece7537-3838-46bc-b021-ab1db6a10c3e
📒 Files selected for processing (7)
.github/workflows/ci.yml.github/workflows/publication.ymldocs/implementation/STATUS.mddocs/trust/PUBLICATION_AUTHORITY.mdfixtures/publication/PilotARefutation.leanscripts/publication-candidate.shscripts/publication-ingest.sh
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 67032b0bc0
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Owner
Author
|
Review follow-up on the two CodeRabbit nitpicks:
|
Owner
Author
|
@codex review |
|
Codex Review: Didn't find any major issues. Keep them coming! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
Owner
Author
|
Merged-tree audit passed for
Full exact identifiers and audit details are recorded on #46. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Prove the independently versioned Pilot A repair, “Every prime number other than 2 is odd,” and carry it through a second protected publication candidate in the same canonical state as the refutation and atomic repair.
The candidate generator now has an explicit
repaired-proofmode. It must load the exact repaired object/version from the retained repair, observenot_startedwith no witnesses, reuse the original registered module and environment, and keep its retained closure inside the original instance. The publication workflow separately attests and ingests that proof candidate, creates distinct proof authority andclaim-relation fidelity, derivesproved, then re-reads the original claim/package/repair and requires byte-identical results.Refs #46, #44, #25.
Change class
Select one:
Affected trust boundary: protected candidate construction, retained-closure containment, attestation ingestion, proof-authority promotion, role-separated statement fidelity, and derived claim status.
TDD evidence
Red evidence: the first elaborating proof used
Nat.mod_two_eq_zero_or_one; the real CLI axiom audit reported[propext], which the protected no-axiom boundary correctly rejects. The first remote simulated candidate also rejected an array-valued semantic metadata field as outside the closedartifact_metadata/1contract.Green evidence: the proof now reasons from
Nat.mod_lt, eliminates the only impossible remainder structurally, and#print axioms MathOS.PilotA.every_prime_other_than_two_is_oddreports no axioms. The module metadata uses separate schema-valid string fields and a real CLI ingest confirms the exact snapshot. PR CI also attempts a repaired candidate before repair and requires a closed failure. A real Windows CLI lifecycle elaborated and audited the exact declaration, prepared a canonicalproofrequest, kept the non-authoritative claimopen, and rejected a mismatchedrefutationrequest.Commands and results:
Local results: 140 unit, 12 CLI integration, 3 MCP integration, the Lean worker baseline, and 39 legacy Python tests passed.
Mathematical verification
Verifier and result: pinned Lean 4.32.0 elaborates the no-import theorem and reports an empty axiom surface. Current-head local CLI request
6a4b6cebdc61631f59e86a158f2cb2e89760904647d66c12bd14065a12e68941is non-authoritative evidence only. Independent candidate/attestation evidence remains intentionally unchecked until the protected merged-tree artifact exists.Provenance and licensing
Provenance references: repository-owned theorem, scripts, workflows, and documentation only; existing pinned Lean, GitHub Actions, GitHub CLI, audit, and publication policies remain unchanged.
Risk and recovery
Known limitations: pull-request CI can elaborate and axiom-audit the repaired theorem and prove that repair is required, but only protected
maincan ingest the first attestation, create the canonical repair, and construct the positive child candidate.Rollback or recovery plan: revert this commit to restore the single refutation candidate. Existing refutation authority, package, claim versions, and repair edges are immutable and are not rewritten by this change.
Follow-up work: independently audit the merged protected artifact before closing #46, then implement Pilot A pedagogy and export.
Review readiness