Repository navigation
feat(proofs): Provenance.Warrant, the signature SoundWarrant and the consent non-upgrade - #164
Conversation
…consent non-upgrade proofs/agda/Provenance/Warrant.agda instantiates epistemic-types' Warrant / Epi / SoundWarrant, imported by pin (6a68de3141a9, fetched by scripts/fetch-siblings.sh; nothing re-declared), with standpoints author, licensor, verifier, consumer. - SignatureVerify.signature-sound: the rule signature-verify makes signed-by sound. The cryptographic assumption (EUF-CMA for the named algorithm) is the module parameter `unforgeable`, not a postulate. ToyModel shows the parameters can be supplied. - ConsentFromHeader: a licence-header token warrants consented-for-training only as Epi. no-consent-sound shows that no soundness map for that warrant exists uniformly (header present, consent absent), and no-transfer shows that a sound warrant for one claim plus a token for another does not give the other (§7.3 rule 6). tests/reject: ConsentFromToken (required by PMP-01), SignatureToConsent (rule 6), AssumptionDropped (rule 3), UnverifiedSignature (rule 7). Each is refused by a type error at its `invalid` declaration. scripts/check-agda.sh checks the positive module first, demands that location and error shape for each rejection, and runs a control: a typechecking variant of ConsentFromToken must be reported as accepted. Kernel flags: --safe --without-K --no-libraries --ignore-interfaces --double-check -W error. CI uses the same pinned debian:13 container and Agda 2.6.4.3 as epistemic-types; checked locally with 2.6.3. signature-verify moves to PROVEN in spec §7.5 and formats/warrant.ncl. The records gate checks that the named proof file exists. PROOF-NEEDS: WL-3 and WL-4 move to PROVEN; WL-7 (no transfer) PROVEN and WL-8 (unchecked signature is not a token) TESTED are added. Refs #162 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9
|
Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configuration
📒 Files selected for processing: 13
✨ Finishing Touches
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
|
CI on this PR: this PR's own jobs pass. The red checks are the same set that is red on
None of these has an existing fix PR I could port. They belong in a separate CI-hygiene change, not in this stack. Generated by Claude Code |
…pass its tests, run it in CI (#165) ## Summary PR B1 of the PMP-01 stack, after #163 and #164 (both merged). PMP-01's validator work (B2: a level per claim, plus the signature-chain fixture) goes into `TOOLS/validation/haskell`. That validator **has never compiled**, and no workflow built it: - With GHC ≥ 8.8, `-Werror=missing-deriving-strategies` fails every `deriving` clause. - `Metadata.hs` is written against aeson 1 (`HashMap` objects, list-typed arrays). - `Reference.hs` has an ambiguous `ClauseReference`. - `License.hs` calls a nonexistent `T.decimal`. - `validateClauseStructure` is exported but never defined. - The test suite has never compiled either. This PR makes the existing validator build and pass its own tests, then runs it in CI. It adds no features. Four commits, each reviewable on its own: 1. **`fix(validator): build … under GHC 9.4 and aeson 2`**: compile fixes only. - `DerivingStrategies` in `default-extensions` (the `-Werror` flag is kept). - The aeson-2 `KeyMap`/`Vector` migration, the missing imports, and the test modules' compile fixes. - Helpers the tests call are now exported. - Unused dependencies reported by `-Wunused-packages` are removed. `hspec-discover` is removed because `Spec.hs` lists its modules explicitly. - `extra-source-files` now names the README that exists. - Zero warnings. 2. **`fix(validator): resolve the test failures where code or test is wrong`**: 17 of the 284 examples failed. For each I decided which side was wrong and fixed only that side: - **Code was wrong:** `titleMatches` (em-dash spacing), `parseTableRow` (separator and malformed rows), `extractClauseNumber` (lower case, multi-level numbers), `parseClauseNumber` (trailing garbage). - **Test was wrong:** the E2E "own content" test looked in the heading instead of the content; a QuickCheck generator contradicted two other tests. - **Harness:** `Spec.hs` sets UTF-8, so E2E tests don't depend on the machine's locale. 3. **`ci(validator)`**: new job `validator` in `.github/workflows/warrant.yml`. - It uses Ubuntu 24.04's own GHC 9.4.7 and cabal 3.8.1 and the `libghc-*-dev` packages, with **no Hackage**: the cabal config has no repository, and `/usr/bin/cabal` and `with-compiler: /usr/bin/ghc` are named explicitly so a ghcup toolchain on `PATH` can't take over. 4. **`fix(validator): meet the six remaining test expectations`**: six tests assert behaviour the code lacked. Each fix is local: - `extractClauseRefs` matches "clause" in any case and skips `#` heading lines, since a heading defines a clause rather than referring to one. - `extractVersion` matches "version" in any case, and as a last-tried pattern takes a bare number after "License". - `detectLanguage` knows four more keywords. - `extractURLRefs` also takes bare URLs, once markdown links are removed. **No test was deleted, skipped, marked pending or weakened.** ## Type of Change - [x] Bug fix - [x] Other (CI job) ## Related Issues #162 (prerequisite for its validator item) ## Files Updated `TOOLS/validation/haskell/{palimpsest-validator.cabal, src/**, app/Main.hs, test/**, bench/ValidatorBench.hs, .gitignore}`, `.github/workflows/warrant.yml`. ## Provenance Notes - Origin: PMP-01 proposed-work item 3. The issue's open question asks whether the Haskell validator stays. This PR keeps it, as PROMPT.md asked, and makes it real. - `stack.yaml` (lts-20.26) is untouched and **untested**. Stack never built this code either. CI uses cabal with apt packages. ## Checklist - [x] SPDX headers present (new `.gitignore` included) - [x] Commit messages follow schema ## Additional Context **Local gate (GHC 9.4.7, cabal 3.8.1, apt packages, no Hackage):** ``` cabal build all --enable-tests → 0 errors, 0 warnings cabal test --test-show-details=direct 284 examples, 0 failures ``` I also ran it with `--seed` 1, 42 and 98765 and `--qc-max-success=500`, with the same result. **Left alone, noted for the owner:** - `-fhpc -hpcdir dist/hpc` in the test stanza: a leftover `.tix` aborts the next local run. CI is unaffected. I suggest `cabal test --enable-coverage` instead. - The validator still expects the old layout (`LICENSES/v0.4/…`, `## Clause N` headings). Today `project` validates only `metadata/palimpsest.jsonld`. - The library reads files with the locale encoding. - `findBrokenLinks` returns every reference, not just broken ones, and `validateClauseRef` is a placeholder. - The benchmark doesn't build (NFData, a name clash); it isn't enabled. - The cabal file and the package `LICENSE` say MIT, while the sources carry PMPL headers. - `.stack-work/` is tracked in git. - Many tests assert on literals without exercising the validator. **Known CI context:** the same checks that are red on `main` will be red here. #164 has a comment listing them. Two more, not from this stack: - "Check external links": its lychee download URL returns 404. - "Security / CodeQL Analysis (python)": already red at `bd13ce7`. **Stack:** #163 A (merged) → #164 C (merged) → B1 (this) → B2 validator levels and fixture → D `pmpl-verify` levels → E press-text correction. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9 --- _Generated by [Claude Code](https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
) ## Summary PR B2 of the PMP-01 stack, **stacked on #165**, so the base is B1's branch. It meets PMP-01's acceptance criterion: "a fixture shows a valid signature chain at `sound` and the consent claim at `epi` on the same artefact". ``` $ palimpsest-validate provenance tests/warrant/fixture/poem.txt.provenance.json sound signed-by ed25519:0d4179…fd30: verified, assuming EUF-CMA security of the signature algorithm named in each signature sound signed-by ed25519:9cee09…520f: verified, assuming EUF-CMA security of the signature algorithm named in each signature epi licensed-under PMPL-1.0-or-later: evidence present (spdx-header poem.txt:1), not verified epi consented-for-training poem.txt: evidence present (licence-header poem.txt:3), not verified 4 claims: 2 sound, 2 epi, 0 warrant; 0 failed ``` **What changes** - `Validator/Types.hs` gains `WarrantLevel = LevelWarrant | LevelEpi | LevelSound`. - `Validator/Provenance.hs` reads a provenance file: an Ed25519 signature chain over the artefact, plus the claims it makes. - **`signed-by`** (one claim per chain entry) is `sound` only when three checks pass: the entry binds the artefact's SHA-256, it links to the previous entry's record, and its signature verifies. The rule is `signature-verify`, whose entailment `Provenance.Warrant` (#164) proves with EUF-CMA as a module parameter. - A signature in an algorithm the tool can't check is held at **`epi`**. - A failed check is **FAILED and held at `warrant`** (§7.3 rule 7). - **`licensed-under` / `consented-for-training`** are `epi` when the declaring header is present and `warrant` otherwise. The function that decides them has no `sound` case. - CLI: `palimpsest-validate provenance FILE [--json]`. - Only `sound` lines say "verified". - `--json` emits records in the shape `formats/warrant.ncl` checks. - The exit status is non-zero only when a check fails, never because a claim is below `sound`. - Fixture `tests/warrant/fixture/`: - `poem.txt` and a two-entry chain (author, then licensor). - `regenerate.sh` rebuilds the chain with throwaway OpenSSL keys, so **no private key is committed**. - `expected.json` is the validator's `--json` output. The Haskell tests require the validator to reproduce it exactly, and the Nickel records gate checks it against the contract and its levels. That links the two gates through one committed file. ## Type of Change - [x] Other (validator feature, fixture, CI packages) ## Related Issues #162 ## Files Updated `TOOLS/validation/haskell/{src/Palimpsest/Validator/{Provenance,Types}.hs, app/Main.hs, test/{Spec.hs, Palimpsest/Validator/ProvenanceSpec.hs}, palimpsest-validator.cabal, README.adoc}`, `tests/warrant/fixture/*`, `scripts/check-warrant-records.sh`, `.github/workflows/warrant.yml`, `PROOF-NEEDS.adoc`. ## Provenance Notes - Signature algorithm: the fixture and the validator use Ed25519, the classical algorithm in §3.1, because it is what Ubuntu's Haskell packages (crypton) and OpenSSL provide. The rule itself is stated for any algorithm. Choosing algorithms stays out of scope, per the issue. - The link between crypton's Ed25519 and the proof's `verify` parameter is **ASSUMED** (WL-10). The fixture's OpenSSL-made signatures verify under crypton, which shows two implementations agree; it is not a proof. ## Checklist - [x] SPDX headers on every new file that takes comments - [x] gitleaks (8.16, default rules) finds nothing in the fixture; `shellcheck` is clean; the invisible-character scan is clean ## Additional Context **Local gates** ``` cabal build all --enable-tests → 0 errors, 0 warnings cabal test --test-show-details=direct → 294 examples, 0 failures (also from a clean copy with the CI cabal config, a fresh CABAL_DIR and LANG unset) bash scripts/check-warrant-records.sh PASS: validator fixture conforms (signed-by=sound,signed-by=sound,licensed-under=epi,consented-for-training=epi) … PASS: warrant records, spec example, coverage and all 11 expected rejections ``` **Tests** (`ProvenanceSpec`, 10 examples): - the fixture's levels, and its output matching `expected.json`; - only `sound` renders as "verified"; - a changed artefact, a forged signature, a valid signature under another key and a broken parent link each FAIL and are held at `warrant`; - an unknown algorithm is held at `epi`; - a consent claim without its header is held at `warrant`; - a QuickCheck property: no licence or consent claim reaches `sound`, whatever the artefact says. **Negative control:** making a header give its claim `sound` fails 4 of these tests. **Status rows** (`PROOF-NEEDS.adoc`): - WL-5 validator → TESTED; - WL-9 `pmpl-verify` → DESIGNED (next PR); - WL-10 crypton implements `verify` → ASSUMED. **Stack:** #163 (merged) → #164 (merged) → #165 B1 → B2 (this) → D `pmpl-verify` levels → E press text. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9 --- _Generated by [Claude Code](https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
…167) ## Summary PR D of the PMP-01 stack. #166 has merged, so this PR's base is now `main`. It meets the acceptance criterion "`pmpl-verify` emits `level` for every claim" and the new §5 MUST. **Before this PR:** `pmpl-verify` recomputed the SHA3-256 content hash, then printed **`OK: <path>`**, and its directory summary counted these as **"Verified"**. It never checks the cryptographic signature. A `TODO: Verify cryptographic signature when PQC libs are integrated` has been there since the tool was written. Under §7, that output is a bare pass for a claim that is at most `epi`. **Now** each signed file yields one `signed-by` claim at its level: - Hash matches: **`epi`**, printed as `evidence present (signature …, content hash matches; pmpl-verify does not check ML-DSA-65 signatures yet), not verified`. - Hash differs: **FAILED**, held at `warrant`. A signature over other content is not a token for this file. - `--existence-only`: **`epi`**, with the content hash not checked. This needs a parseable signature block and an existing artefact. An empty or malformed `.sig` gives no claim. - The summary counts claims by level (sound / epi / warrant), plus failed, unsigned and errored files. - Exit codes are unchanged (non-zero when a claim fails), so the GitHub and GitLab integration templates behave as before. - `Level::Sound` exists for when signatures are verified (rule `signature-verify`). Nothing produces it today. - Values read from the signature file (signer, algorithm, hashes) and the file path are printed with control characters escaped. A `\r` or terminal escape can't rewrite the level shown on the line. `tools/README.adoc` no longer says the tool verifies signatures. A CI job, `warrant.yml / pmpl-verify reports a level per claim`, runs `cargo test`. It was added because `ci.yml` runs only for PRs into `main`, which this PR wasn't until now. ``` FAILED signed-by ML-DSA-65:author@example.org …/b.txt: content hash does not match the signature (expected 0000…, actual 81e0…); held at warrant epi signed-by ML-DSA-65:author@example.org …/a.txt: evidence present (signature …/a.txt.sig, content hash matches; pmpl-verify does not check ML-DSA-65 signatures yet), not verified Summary: 2 claims sound: 0 epi: 1 warrant: 0 failed: 1 unsigned: 1 errors: 0 ``` ## Type of Change - [x] Bug fix (a bare pass for an unverified signature) - [x] Documentation update ## Related Issues #162 ## Files Updated `tools/pmpl-verify/src/main.rs`, `tools/README.adoc`, `.github/workflows/warrant.yml`, `PROOF-NEEDS.adoc`. ## Provenance Notes - The older "What Needs Proving" row in `PROOF-NEEDS.adoc` for `pmpl-verify` ("Signature verification is correct") describes a check the tool doesn't perform yet. This PR makes the output say so; it doesn't add PQC verification. ## Checklist - [x] SPDX headers unchanged/present - [x] Commit messages follow schema ## Additional Context **Local gate** ``` cargo test (tools/pmpl-verify) → test result: ok. 13 passed; 0 failed ``` What the tests cover: - A matching hash is `epi` and renders "not verified". - A mismatch fails at `warrant`. - `--existence-only` gives `epi` for a parsed block. - An unsigned file makes no claim. - An empty sidecar makes no claim. - A signature with no artefact makes no claim. - Control characters in `Signer` are escaped. **Negative controls**, each reverted after the run: - Returning `Sound` for a matching hash fails the `epi` test. - Dropping the escaping fails the escape test. - Restoring the old early return in existence-only mode fails three tests. **Review (CodeRabbit):** both Major findings are fixed in `8122605` and their threads resolved. The replies in those threads name `ed843f7`; that was the same commit before I rebased it onto the branch after it was rebased on GitHub. - CWE-117: control characters are now escaped. - CWE-20: no `epi` without a parsed signature. The docstring-coverage pre-merge warning is addressed by doc comments on the functions this PR touches. `cargo clippy` reports one warning, `&PathBuf` instead of `&Path`, in a function signature that predates this PR. The original file wasn't rustfmt-clean either, so I didn't reformat lines I hadn't touched. **Status row:** WL-9 → TESTED. **Stack:** #163, #164, #165 and #166 are merged → D (this) → #168 E press text. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9 --------- Co-authored-by: Claude <noreply@anthropic.com>
## Summary PR E of the PMP-01 stack, **stacked on #167**. It meets the acceptance criterion "No README or press text describes a consent claim as verified". I searched `README.adoc`, `README.nl.adoc`, `press-lobby-kit/`, `campaigns/press/`, `OUTREACH/`, `PRESENTATION/` and `docs/` for consent described as verified, validated, proven or guaranteed. The only README or press text that did so is `press-lobby-kit/video-scripts/technical-deep-dive-30min.adoc`. Three passages change: - The learning objective "*Deploy* Haskell validators for consent verification" now reads "*Deploy* Haskell validators that report each consent claim at its warrant level (a declared consent is evidence, never verified consent)". - In the code walkthrough, the `Granted` reason "Creator has granted consent for AI training" (read straight from a metadata field) becomes "Metadata declares consent for AI training (evidence, not verified)". - The voiceover "The creator allows AI training" becomes "The metadata declares that the creator allows AI training. That declaration is evidence, not verification: the validator reports it as 'evidence present, not verified', never as verified consent." The rest of the script is unchanged: `Denied` and `Pending`, the registry stub, and the timing. ## Type of Change - [x] Documentation update ## Related Issues #162 ## Files Updated `press-lobby-kit/video-scripts/technical-deep-dive-30min.adoc` ## Provenance Notes - Basis: `spec/PROVENANCE-SPEC.adoc` §7.3 rule 4 (no rule entails `consented-for-training`) and rule 5 (no bare pass below `sound`). ## Checklist - [x] AsciiDoc validated (`asciidoctor --failure-level=WARN`) - [x] Commit message follows schema ## Additional Context **Left for the owner to decide:** `campaigns/consent-layer/*` uses "verify consent" for a proposed registry lookup. Examples are `GET /consent/verify` and "Block API access if consent not verified". These are design documents for a system that isn't built yet, not README or press text, so I haven't changed them. Under §7, a registry receipt is `epi` for consent; only its signature can make `signed-by` sound. Whether to reword them is the owner's call. **Stack:** #163 (merged) → #164 (merged) → #165 (merged) → #166 B2 → #167 D → E (this). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9 --- _Generated by [Claude Code](https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9)_ Co-authored-by: Claude <noreply@anthropic.com>
…-apply documentation comments All 11 conflicts were add/add: this branch carried the original warrant work plus a coderabbit documentation commit, while main merged the rebased feature via #163/#164 and 15 later commits. Resolution takes main's side for every conflicted file and re-applies the PR's doc comments on top (formats/warrant.ncl, proofs/agda/Provenance/Warrant.agda), folding the PR's fetch() detail into the existing comment in scripts/fetch-siblings.sh. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>



Summary
PR C of the PMP-01 stack. It follows #163 (merged) and comes before the validator PRs: the validator emits
soundundersignature-verify, and that rule should already be PROVEN at the validator's own head.proofs/agda/Provenance/Warrant.agdainstantiates epistemic-types'Warrant/Epi/SoundWarrant. The sibling is imported by pin:6a68de3141a981d766fd006b312f0919ade334bf, fetched by the newscripts/fetch-siblings.sh(the residual-evidence-types pattern) and recorded in the module header. Nothing is re-declared, and the empty type is epistemic-types' ownImpossible. Standpoints areauthor,licensor,verifierandconsumer.SignatureVerify.signature-soundmakessigned-bysound. Its evidence type is "a signature together withverify pk m σ ≡ true". The cryptographic assumption, EUF-CMA for the named algorithm, is the module parameterunforgeable, not a postulate (--safeforbids postulates anyway).ToyModel.exampleshows the parameters can be supplied, so the rule is not vacuous; the module says plainly that the toy is not a signature scheme.ConsentFromHeadergives a licence-header token only anEpiforconsented-for-training. Two theorems back this:no-consent-sound: no soundness map for that warrant can be given uniformly. Where a header is present and consent was not given, it would inhabitImpossible. This is epistemic-types'no-receipt-reflection(E-2) specialised to consent.no-transfer(§7.3 rule 6): a sound warrant for one claim, held with a token for another, does not give the other.tests/reject/. Each is refused by a type error at itsinvaliddeclaration:ConsentFromToken:Header x !=< Consented x.SignatureToConsent:SignedBy pk m !=< Consented x.AssumptionDropped:verify pk m σ ≡ true !=< SignedBy pk m.UnverifiedSignature:(verify pk m σ) != true.scripts/check-agda.sh. It typechecks the positive module first, so a missing import can't pass as a rejection. For each fixture it requires an error located at or after theinvalid :line, with "when checking that" and none of "Not in scope / Failed to find / Unsolved / Parse error". A built-in control derives a valid variant ofConsentFromToken, checks that it typechecks, and checks that the harness reports it as accepted.signature-verifymoves to PROVEN in spec §7.5 and informats/warrant.ncl. The records gate from #163 already checks that the contract and spec agree and that a PROVEN rule's proof file exists.Type of Change
Related Issues
#162
Files Updated
New:
proofs/agda/Provenance/Warrant.agda,tests/reject/{ConsentFromToken,SignatureToConsent,AssumptionDropped,UnverifiedSignature}.agda,scripts/fetch-siblings.sh,scripts/check-agda.sh.Changed:
spec/PROVENANCE-SPEC.adoc(§7.5 status),formats/warrant.ncl(rule status),PROOF-NEEDS.adoc,.github/workflows/warrant.yml(newagdajob),Justfile(fetch-siblings,agda),.gitignore(*.agdai).Provenance Notes
6a68de3(the head the issue verified against; choreographic-types still pins495db9c).unforgeableis supplied.Governance Impact
Checklist
PROOF-NEEDS.adoc, spec)shellcheckcleanAdditional Context
Gate output (local, Agda 2.6.3):
Negative controls, each run and then reverted:
ConsentFromTokenwith a valid body fails the gate:invalid proof accepted.SignatureToConsentfails it:not by a type error at its invalid declaration.Agda version: CI runs Agda 2.6.4.3 in the same digest-pinned
debian:13-slimcontainer as epistemic-types' Proof Safety job. I could only check locally with Ubuntu's 2.6.3, because the Debian mirror is blocked from this environment. So this PR'sagdajob is the first 2.6.4.3 run of the module.Status rows moved (
PROOF-NEEDS.adoc):SignatureVerify.signature-sound.no-consent-sound, plus theConsentFromTokenfalsifier.no-transfer, plusSignatureToConsent.UnverifiedSignature.Stack: #163 A (merged) → C (this) → B1 validator build repair → B2 validator levels and fixture → D
pmpl-verifylevels.🤖 Generated with Claude Code
https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9
Generated by Claude Code