Repository navigation
WIP: finish mathematical implementation and verification infrastructure (certify in successor PR) - #113
Draft
HMarcusWH wants to merge 597 commits into
Draft
WIP: finish mathematical implementation and verification infrastructure (certify in successor PR)#113HMarcusWH wants to merge 597 commits into
HMarcusWH wants to merge 597 commits into
Conversation
…ueness; record immutable tooling gate
… in immutable T/B/H
…ed successor proposal
…olean simplification
…very test fixtures
…out altering providers
…er unittest method
…ources at same head
…er dossier from authenticated CI producers
…s to authentic producer jobs without v2 self-approval
…ped test receipts Preserve frozen mathematics and historical CI policy. Add early research-Python syntax regression, reject unowned candidate receipts, and permit claim-only positive/negative tests without manufacturing approvals.
… profile Audit the exact former-provider Git delta while preserving the original A2 historical verifier and four kernel-checked Lean proof blobs. Explicitly fail closed on changed workflow/security/test providers, dependency pins, source shadows, missing imports or missing independent approval. No historical gate is relaxed or replaced.
… acceptance Fail closed when executable verification, research release, Windows integrity or either application contract fails or is missing. Add source-bound negative regression tests. Historical T verifier and approval records remain untouched.
…audit Permit only two explicitly located formatting-only blank lines after the original A2 proof imports. Any change to import content, theorem provider, or other root bytes still fails closed. Versioned successor remains unapproved.
…ducing ZIP artifacts
…artition for all 76 owners
…inks/nonregular sources
…urce-symlink evidence inputs
…t security review
… authorized activation
…al v3 regressions
…e30 A2 source OIDs
…iagnostics Preativation FINAL-01 to FINAL-04 implementation candidate. Preserve original 25 workflows and historical T/A2 authorities. No workflow activation, evidence approval, merge or release.
… CI failure Capture the adversarial renderer inside its unittest and assert the expected failure identity without emitting a misleading external failure marker.
…ted regression failures R6-01: validate both installed historical_runtime_v3 call sites while retaining original preactivation archive/T/A2 and historical v2 fragment assertions. R6-02: emit bounded method-level active30 failure diagnostics, secure redaction, source-bound failure receipts, timeout and skip/error negative regressions. Preativation engineering-only; no workflow activation or security approval.
… lifecycle Export one nonauthorizing v3 receipt path for all phases; the staged Research consumer reauthenticates genuine original T/A2 for #113 and inherited M113 for descendants. Reject ambiguous detached JSON and borrowed evidence. Preserve historical A2 executor and workflow installation status. Add synthetic four-phase/negative integration tests and repin the staged test Git blob.
Add synthetic four-phase GITHUB_ENV producer/consumer coverage, reject NaN and overlarge floats in original historical events, and record an explicit noncircular two-stage cutover runbook without granting security, merge or publication authority.
…utant bytes Repair v2 current A2 intake to require source_1 through source_4, full/focused command sets, and only the declared one-step semantic source mutations. Add real consumer negative controls for missing probes, unrelated modified Lean source, parser, import and timeout failures.
Scope original A2 compiler expectations to immutable introducer source. Validate active30's phase-aware required consumer against exact staged Git blob and full 25/30 workflow profile. Replace obsolete v2-only staged assertions; preserve negative no-skip and original A2 historical source identities.
Update the unapproved migration manifest's single stale Git object reference to the revised phase-aware A2 test. Preserve original A2 and all other historical/approval contract fields. Existing original and atomic cutover source guards now enforce the same staged identity.
…light Ensure the phase-neutral four-event Research consumer, historical Git source identity, strict external event JSON and semantic A2 compiler receipt validation are exercised before expensive full research compilation. No historical verifier or protected workflow changes.
…xtures Bind staged A2 identity to committed Git bytes and unapproved R3 manifest rather than obsolete blob literals. Run complete four-mutant/four-source diagnostic fixtures through the real v2 receipt validator, retaining negative parser/import/resource controls. Add the boundary suite to exact-head fast QA. Preserve historic T/A2 and 25 active workflows.
Replace assertion-only M113 child checks with explicit runtime validation of twelve exact-H successful check identities, original independent security review, historical-only CI scope and producer/reviewer IDs. Add optimized-Python synthetic rejection controls to fast preflight. No historical source or active workflow alteration.
…ow cutover Select the native v1 or v2 compiler only after the complete exact-Git source-profile audit. Preserve the original 40 declarations and four semantic controls, reject source drift and never fall back after failure. Add 13 routing regressions, register them in the 53-suite preflight, and consolidate the source/evidence/approval/activation sequence required for merge readiness. Historical verifiers, active workflows, reviewer authority and merge state are unchanged.
Owner
Author
Consolidated merge-completion plan and source repairPushed New defect repaired: the mandatory current-source A2 Lean test always selected the v1/25-workflow compiler. It would reject the installed 30-workflow configuration. It now selects v1 or v2 only after the complete exact-Git workflow-profile audit. Both native compilers and historical A2 remain unchanged. There is no fallback after an audit or compiler failure. Verification: 13 routing tests passed locally in normal Python and the same 13 passed under Remaining merge dependencies: genuine preactivation historical evidence; real owner-authorized independent reviewer roster; independent source-security review and separate installation authorization; atomic ten-path cutover; genuine final-head T/A2 producer artifacts and artifact-bound independent approval; all twelve required contexts and applicable downstream Research steps; effective main protection and separate owner merge decision. This comment is an engineering handoff, not an approval. No protected workflow was activated, no reviewer identity fabricated, and no merge or publication performed. CERT retains independent mathematical/scholarly acceptance. |
…02 compilation Replace the mismatched current-head historical integration with mandatory fresh historical and current-source compiler legs. Execute the immutable original gate in a clean detached historical checkout, share only verified pinned dependencies, prohibit historical project-build reuse, validate complete receipts and retain failure diagnostics. Preserve the registered P02 method's current-source coverage and the standalone native successor test. Reconcile exact integration pins and staged/active source guards together; add 13 real-Git protocol regressions and the 54th fast preflight suite. No installed workflow, original executor, Lean proof, dependency pin, archive verifier, reviewer authority or merge setting is changed. Research green remains actual-CI evidence, not historical migration approval or merge authorization.
Owner
Author
Research source-target repair deployed —
|
…pport blob Keep both revisions exactly pinned, including historical localized_prefix_support b07bc7d and current 93462e9; preserve the unchanged gate binary and original integration source. Recreate real synthetic two-revision support drift in 16 replay tests, add negative historical/current substitution and an authentic Git source-object pin test. No workflow, accepted evidence, Lean theorem or security approval changed.
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.
Revised scope — implementation and verification infrastructure
PR #113 completes the promised mathematics, implementation, historical/security compatibility and working verification/release tools. Full independent mathematical certification and publication happen in a successor PR (temporary label: CERT).
This replaces the earlier single-PR completion sequence. It does not relax the mathematical requirements or claim that an unfinished proof is certified. The original 45 acceptance cases, 11 mathematical claims, historical T/A2 checks, baseline 259-declaration inventory, accepted release bytes and protected core/pins remain authoritative.
Implementation scope for #113
Deferred to successor CERT (not waived)
Approval/status boundaries
Branch:
research/final-mathematical-closure. Original base:17c315f7df7abf457eb94d393bd526d46da6f6f4. The actual current head must be obtained from GitHub; old SHA-labelled results are historical only.Successor numbering: GitHub #114 is already a closed repair PR merged into this branch. The certification PR will be opened after a real authorized #113 merge, and GitHub's actual new number will be used.
Operational handoff:
docs/operations/pr113_implementation_scope_and_certification_handoff.md(the split's 13 implementation steps and 11 certification steps).Do not merge or tag without a separate owner decision.