Skip to content

Integration: accept Muse-authored payout repair - #2

Closed
davidwilliam wants to merge 5 commits into
mainfrom
integration/accepted-repair
Closed

davidwilliam wants to merge 5 commits into
mainfrom
integration/accepted-repair

Conversation

@davidwilliam

Copy link
Copy Markdown
Owner

Integration test: install the stored Muse-authored payout repair from muse-repair-002.

Expected result: all eight locked requirements are VERIFIED and the rebuilt binary passes. The action must produce a fresh Proof Passport and a PR comment. This test PR is not intended to merge.

@github-actions

Copy link
Copy Markdown

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:b84b81d22511ce42  PASS (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:120f7de43f50aa38  Passport sha256:fb45c8f6c9aadc0b

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

Proof check rejected:

  • error: Child exited with 1

@github-actions

Copy link
Copy Markdown

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:b84b81d22511ce42  PASS (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:120f7de43f50aa38  Passport sha256:5662631855fa601f

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

Proof check rejected:

  • error: Child exited with 1

@github-actions

Copy link
Copy Markdown

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:d85a158bd1cdb4b9

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

@github-actions

Copy link
Copy Markdown

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:576d0043fa123d1e

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

@github-actions

Copy link
Copy Markdown

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:1c506a7535a16d91

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

@davidwilliam davidwilliam added the gate-demo Demonstration of the ProofForge pull request check; not for merging label Nov 3, 2026
@davidwilliam

Copy link
Copy Markdown
Owner Author

Demonstration of the ProofForge pull request check, kept as evidence and closed without merging. The check accepted the Muse-authored payout repair and issued a VERIFIED Passport. Recorded outcomes: reports/pr-integration/summary.json.

@github-actions

github-actions Bot commented Nov 3, 2026

Copy link
Copy Markdown

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:2d7a4c8688d198d2

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

gate-demo Demonstration of the ProofForge pull request check; not for merging

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant