test(aggregate): ideal Idris2 proof fixture + end-to-end fold test#138
Merged
Conversation
aggregate folds external prover output (incl. Idris2) but had NO proof fixture and no end-to-end fold test (only annotation/spec unit tests). proven has Idris2 files, but they are library property-tests, not detector-soundness proofs in aggregate's shape. Adds tests/fixtures/proofs/UnsafeCodeSoundness.idr: a genuine idris2 --check clean, %default total proof (no escape hatches) of the UnsafeCode (PA001) detector's soundness AND completeness, carrying the @name and @Covers sound:category:UnsafeCode annotations aggregate reads. And tests/aggregate_proof_fixture.rs: folds it via aggregate::run and asserts it is recognised as Idris2, classified Closed (no holes), hashed, named, and that the coverage parses to Sound/Category/UnsafeCode. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 24, 2026
…k) (#139) The pre-commit licence enforcer (`.git/hooks/pre-commit`) requires **both** `SPDX-License-Identifier: MPL-2.0` **and** the exact owner string `Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>` on every staged source file — but **no `.rs` file carried the owner line**. Every `.rs` had the SPDX identifier on line 1, yet the owner check (stricter than the existing tree) meant any future edit to a `.rs` file was blocked by the hook. Surfaced while fixing the audience→axial doc drift (#137). ## Changes - Inserts `// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>` on line 2 of all **91 tracked `.rs` files** (each already had the SPDX identifier on line 1). - Renames the cosmetic `audience.md` temp filename in the `axial` test to `axial.md`, completing the audience→axial sweep. Comment-only changes plus one test-string rename. `cargo check --all-targets` passes; the licence-enforcer hook now passes on `.rs` edits (this commit itself passed it with hooks enabled). Out of scope (noted, not done): `.md`/`.adoc`/`.idr` source files — the two header-less docs are handled in #137 and the new Idris2 fixture in #138 already carries the header; a follow-up can extend the same owner line to remaining non-`.rs` sources if wanted. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
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
1 participant
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.
aggregatefolds external prover output (Agda/Idris2/Coq·Rocq/Lean/Isabelle/SMT) into a report, but had no proof fixture and no end-to-end fold test — only annotation/spec unit tests.provenhas Idris2 files, but they are library property-tests, not detector-soundness proofs inaggregate's shape.Changes
tests/fixtures/proofs/UnsafeCodeSoundness.idr— a genuineidris2 --check-clean,%default totalproof (no escape hatches: nobelieve_me/assert_total/idris_crash/postulate, no metavariable holes) of the UnsafeCode (PA001) detector's soundness and completeness, carrying the@nameand@covers sound:category:UnsafeCodeannotations the folder reads.tests/aggregate_proof_fixture.rs— folds the fixture viaaggregate::runand asserts it is recognised asIdris2, classifiedClosed(no holes), hashed (non-repudiation), named from@name, and that the coverage parses toSound/Category/UnsafeCode.Verified:
idris2 --checkexits 0;cargo test --test aggregate_proof_fixturepasses (1 passed).🤖 Generated with Claude Code