Repository navigation
proofs: write the receipt under the new PROOF-POLICY 8.5 and add APP-1 to APP-4 - #90
Draft
hyperpolymath wants to merge 3 commits into
Draft
hyperpolymath wants to merge 3 commits into
hyperpolymath wants to merge 3 commits into
Conversation
…1 to APP-4 Standards PRs 1534 and 1545 (merged at e5a39d7, owner rulings 2026-11-13) make every current receipt record its inputs manifest, its inputs digest and its axioms, add echo records for squash and rebase merges, and give the home gate and consumers a shared git checker (PROOF-POLICY 8.5.3). - verification/receipts/theory_praxis.deed: written again from CI run 43498592499 on main 034f215. THY-1 is earned again, and APP-1 to APP-4 are added, each with Agda, Rocq and Lean legs. One manifest per prover: the union of the files that the graded roots read. The trusted base gains Char and String, which Applied/IntLaws reaches through Agda.Builtin.Int. The reader at e5a39d7 derives PWG-1 for all five. - just receipt-check (in just check): the home gate runs the shared checker on this receipt against origin/main. CI fetches the history of main, and the pinned Guix shell gains jq, which the checker needs. - The registry pins the reader at e5a39d7 and the checker scripts by digest. It catalogues a PWG-1 only when the git checks hold against a clone of the home repository; otherwise PWG-2ii, with the reason (ADR 0004 amended). - THY-1 shows as ungraded until its claim pin moves to this receipt in the next change; the theory ledger records it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| // instead of fetching them (the tests use it; CI fetches). | ||
| import {readFile, writeFile, mkdir} from 'node:fs/promises'; | ||
| import {readFile, writeFile, mkdir, mkdtemp} from 'node:fs/promises'; | ||
| import {spawnSync} from 'node:child_process'; |
Owner
Author
There was a problem hiding this comment.
Traced, not yet dismissed: this is a security finding, so it stays open for the owner's decision.
The import serves the PROOF-POLICY §8.5.3 duty, which needs git. Every call is spawnSync(program, argv) with no shell option, so no shell parses the arguments.
- Since bdcc599, each program (
git,bash) runs by its absolute path, found only in absolute directories of PATH (findTool). - The arguments are constants, temporary paths that this process makes, the checker path (pinned by sha256 in
CHECKER), andhttps://github.com/<repo>. <repo>comes from a claim pin thatvalidate()limits to^[-\w.]+\/[-\w.]+$and to repositories that the census lists as public.
The same pattern in scripts/site/site.mjs carries hypatia:ignore js_exec_sync (commit 493dd9c). I will add the same annotation here only if the owner rules for it.
Generated by Claude Code
The Proven test suite pinned its own checkout of the reader at be39f90, which refuses the new :inputs-sha256 field (run 43513006338). Pin it at e5a39d7, the commit the registry pins, and add the two checker scripts that the registry's git checks need to its sparse checkout. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk
…loop Answers the SonarCloud findings on the git checks: S4036 (a program found through PATH), S3776 (deriveAll too complex) and S9382 (await in a loop). Each program now runs by its absolute path, found in an absolute directory of PATH, as scripts/site/site.mjs does for asciidoctor. deriveAll reads each distinct receipt once, derives, then runs each needed git check once. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk
|
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
This rewrites the Mathesis receipt under the new PROOF-POLICY §8.5.1 to §8.5.3, which standards PRs 1534 and 1545 merged at
e5a39d7(owner rulings 2026-11-13). The receipt adds APP-1 to APP-4 and earns THY-1 again. The canon reader ate5a39d7derivesPWG-1for all five. The new shared git checker passes on this receipt.This is the first of two changes. The claim pins can name this receipt only after it is on main, so the next change moves them.
Changes
verification/receipts/theory_praxis.deed: written again from CI run 43498592499 on main034f215(Agda 2.7.0.1, Rocq 8.18.0, Lean 4.29.0, pinned Guix8edb9da).Applied/Missing.agdafor APP-1 and APP-4, andApplied/IntLaws.agdafor APP-2 and APP-3. The Rocq leg isCohort.vand the Lean leg isCohort.lean.:inputs-sha256,(axioms)(empty: the run reported none) and(inputs-manifest …). There is one manifest per prover, because §8.5.1 allows one digest for each commit and prover: it is the union of the files that the graded roots read.CharandString.Applied/IntLawsreaches them throughAgda.Builtin.Int. I checked thelib/primsources of Agda 2.7.0.1.just receipt-check, part ofjust check, runs the shared checkerscripts/check-proof-receipt.shagainstorigin/main. CI fetches the history of main, and the pinned Guix shell gainsjq, which the checker needs.e5a39d7, and it pins the checker and the digest script by their digests. It catalogues aPWG-1only when the git checks pass against a clone of the home repository, including its pull-request heads. Otherwise it cataloguesPWG-2iiand records why. ADR 0004 is amended.Known, temporary
ungradeduntil the next change. The new reader refuses the old receipt that THY-1's claim pin names. The theory ledger records this.RECONCILEDby the clause-by-clause comparison in PROOF-STATUS, which I did by reading. The owner has not reviewed it yet.RSR Quality Checklist
Required
As Applicable
docs/status/ROADMAP.adocupdatedPWG-1)Testing
In this session, on main
034f215plus this change, with standards ate5a39d7:deed_lint.js --proof-receipt-json) derivesPWG-1for THY-1 and APP-1 to APP-4.just receipt-checkreports "every check holds".just check-viewspasses. The registry reports "derived from 3 pinned source(s); views match; the theory ledger is current and append-only (2 entries)".validate-claude-md,validate-stateandvalidate-rsrpass. The canon deed lint passes on the deed and the receipt. Every changed AsciiDoc file renders without a warning.just check(now withreceipt-check) and the golden controls in the pinned Guix.Screenshots
Not applicable.
Generated by Claude Code