Repository navigation

Integration: reject seeded bulk-rounding repair - #1

Closed

davidwilliam wants to merge 5 commits into

mainfrom

integration/rejected-repair

Closed

Integration: reject seeded bulk-rounding repair#1
davidwilliam wants to merge 5 commits into
mainfrom
integration/rejected-repair

davidwilliam commented Oct 28, 2026

Owner

Integration test: this seeded bulk-payout repair drops the remainder for seven or more recipients and weakens three proof obligations.

Expected result: ProofForge rejects the repair against the locked requirements, even though its finite property tests pass. This PR is evidence for the gate and is not intended to merge.


          Exercise PR rejection of seeded bulk-rounding repair

e41abf4

github-actions Bot commented Oct 28, 2026

ProofForge: payout-flagship UNRESOLVED

REQ-VALID-SUCCEEDS  UNRESOLVED  
REQ-INVALID-NOOP    UNRESOLVED  
REQ-AUTHORIZATION   UNRESOLVED  
REQ-EFFECTS         UNRESOLVED  
REQ-IDEMPOTENCY     UNRESOLVED  
REQ-NONNEGATIVE     UNRESOLVED  
REQ-FAIR-SHARES     UNRESOLVED  
REQ-CONSERVATION    UNRESOLVED  
Executable payout-sidecar: sha256:7af0da72a9aed5f9  PASS (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:2c95409407592f90  Passport sha256:617c68adea8ba86f

Reproduce: proofforge verify passport.json --candidate pr/formal

Proof check rejected:

error: Child exited with 1


          Check final sandbox and Passport integration

008afba

github-actions Bot commented Oct 28, 2026

ProofForge: payout-flagship UNRESOLVED

REQ-VALID-SUCCEEDS  UNRESOLVED  
REQ-INVALID-NOOP    UNRESOLVED  
REQ-AUTHORIZATION   UNRESOLVED  
REQ-EFFECTS         UNRESOLVED  
REQ-IDEMPOTENCY     UNRESOLVED  
REQ-NONNEGATIVE     UNRESOLVED  
REQ-FAIR-SHARES     UNRESOLVED  
REQ-CONSERVATION    UNRESOLVED  
Executable payout-sidecar: sha256:7af0da72a9aed5f9  PASS (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:2c95409407592f90  Passport sha256:9e1448f1e410d796

Reproduce: proofforge verify passport.json --candidate pr/formal

Proof check rejected:

error: Challenge and solution theorem statement do not match: 'Payout.req_fair_shares'


          Replace rejected seeded repair with verified Muse repair

ff5679d

github-actions Bot commented Oct 28, 2026

ProofForge: payout-flagship VERIFIED

REQ-VALID-SUCCEEDS  VERIFIED    statement sha256:d8ef199351b9
REQ-INVALID-NOOP    VERIFIED    statement sha256:5a0c4f002248
REQ-AUTHORIZATION   VERIFIED    statement sha256:9546dbe11b8d
REQ-EFFECTS         VERIFIED    statement sha256:06d053c0e722
REQ-IDEMPOTENCY     VERIFIED    statement sha256:5b16ad1efc68
REQ-NONNEGATIVE     VERIFIED    statement sha256:c9c71dd7bcd0
REQ-FAIR-SHARES     VERIFIED    statement sha256:f3e3da1e7ab8
REQ-CONSERVATION    VERIFIED    statement sha256:3553d7218bb8
Executable payout-sidecar: sha256:b84b81d22511ce42  PASS (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: Lean paranoid, lean4lean, nanoda, con-leche, con-ron, Lean default
Solution tree sha256:120f7de43f50aa38  Passport sha256:82eb146c57e4e1c5

Reproduce: proofforge verify passport.json --candidate pr/formal


          Recheck seeded rejection with updated Passport integrity

6064c1b

github-actions Bot commented Oct 28, 2026

ProofForge: payout-flagship UNRESOLVED

REQ-VALID-SUCCEEDS  UNRESOLVED  
REQ-INVALID-NOOP    UNRESOLVED  
REQ-AUTHORIZATION   UNRESOLVED  
REQ-EFFECTS         UNRESOLVED  
REQ-IDEMPOTENCY     UNRESOLVED  
REQ-NONNEGATIVE     UNRESOLVED  
REQ-FAIR-SHARES     UNRESOLVED  
REQ-CONSERVATION    UNRESOLVED  
Executable payout-sidecar: sha256:7af0da72a9aed5f9  PASS (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:2c95409407592f90  Passport sha256:b21d1cc03fcf5209

Reproduce: proofforge verify passport.json --candidate pr/formal

Proof check rejected:

error: Challenge and solution theorem statement do not match: 'Payout.req_fair_shares'


          Complete rejected-to-accepted PR demonstration with Muse repair

be104f8

github-actions Bot commented Oct 28, 2026

ProofForge: payout-flagship VERIFIED

REQ-VALID-SUCCEEDS  VERIFIED    statement sha256:d8ef199351b9
REQ-INVALID-NOOP    VERIFIED    statement sha256:5a0c4f002248
REQ-AUTHORIZATION   VERIFIED    statement sha256:9546dbe11b8d
REQ-EFFECTS         VERIFIED    statement sha256:06d053c0e722
REQ-IDEMPOTENCY     VERIFIED    statement sha256:5b16ad1efc68
REQ-NONNEGATIVE     VERIFIED    statement sha256:c9c71dd7bcd0
REQ-FAIR-SHARES     VERIFIED    statement sha256:f3e3da1e7ab8
REQ-CONSERVATION    VERIFIED    statement sha256:3553d7218bb8
Executable payout-sidecar: sha256:b84b81d22511ce42  PASS (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: Lean paranoid, lean4lean, nanoda, con-leche, con-ron, Lean default
Solution tree sha256:120f7de43f50aa38  Passport sha256:f88de11208f99c40

Reproduce: proofforge verify passport.json --candidate pr/formal

davidwilliam added the gate-demo label

davidwilliam commented Nov 3, 2026

Owner Author

Demonstration of the ProofForge pull request check, kept as evidence and closed without merging. The check first rejected the seeded bulk-rounding candidate, then accepted its replacement with the stored Muse-authored repair. Recorded outcomes: reports/pr-integration/summary.json.

davidwilliam closed this

github-actions Bot commented Nov 3, 2026

ProofForge: payout-flagship VERIFIED

REQ-VALID-SUCCEEDS  VERIFIED    statement sha256:d8ef199351b9
REQ-INVALID-NOOP    VERIFIED    statement sha256:5a0c4f002248
REQ-AUTHORIZATION   VERIFIED    statement sha256:9546dbe11b8d
REQ-EFFECTS         VERIFIED    statement sha256:06d053c0e722
REQ-IDEMPOTENCY     VERIFIED    statement sha256:5b16ad1efc68
REQ-NONNEGATIVE     VERIFIED    statement sha256:c9c71dd7bcd0
REQ-FAIR-SHARES     VERIFIED    statement sha256:f3e3da1e7ab8
REQ-CONSERVATION    VERIFIED    statement sha256:3553d7218bb8
Executable payout-sidecar (linux/amd64): sha256:b84b81d22511ce42  PASS (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: Lean paranoid, lean4lean, nanoda, con-leche, con-ron, Lean default
Solution tree sha256:120f7de43f50aa38  Passport sha256:1b598d84a9a82656

Reproduce: bin/proofforge verify passport.json --candidate pr/formal

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels