Skip to content

feat(proofs): Provenance.Warrant, the signature SoundWarrant and the consent non-upgrade - #164

Merged
hyperpolymath merged 1 commit into
mainfrom
claude/new-session-8bfbi9
Oct 14, 2026
Merged

hyperpolymath merged 1 commit into
mainfrom
claude/new-session-8bfbi9

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Summary

PR C of the PMP-01 stack. It follows #163 (merged) and comes before the validator PRs: the validator emits sound under signature-verify, and that rule should already be PROVEN at the validator's own head.

proofs/agda/Provenance/Warrant.agda instantiates epistemic-types' Warrant / Epi / SoundWarrant. The sibling is imported by pin: 6a68de3141a981d766fd006b312f0919ade334bf, fetched by the new scripts/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' own Impossible. Standpoints are author, licensor, verifier and consumer.

  • One SoundWarrant. SignatureVerify.signature-sound makes signed-by sound. Its evidence type is "a signature together with verify pk m σ ≡ true". The cryptographic assumption, EUF-CMA for the named algorithm, is the module parameter unforgeable, not a postulate (--safe forbids postulates anyway). ToyModel.example shows the parameters can be supplied, so the rule is not vacuous; the module says plainly that the toy is not a signature scheme.
  • One deliberate non-upgrade. ConsentFromHeader gives a licence-header token only an Epi for consented-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 inhabit Impossible. 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.
  • Falsifiers under tests/reject/. Each is refused by a type error at its invalid declaration:
    • 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 the invalid : 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 of ConsentFromToken, checks that it typechecks, and checks that the harness reports it as accepted.

signature-verify moves to PROVEN in spec §7.5 and in formats/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

  • Specification update (status column only)
  • Other (Agda proofs, gate script, CI job)

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 (new agda job), Justfile (fetch-siblings, agda), .gitignore (*.agdai).

Provenance Notes

  • Origin: PMP-01 proposed-work item 4 and its acceptance criterion "typechecks under the kernel flags with the sibling pinned; the reject fixture is refused".
  • Pin: epistemic-types 6a68de3 (the head the issue verified against; choreographic-types still pins 495db9c).
  • Open question from the issue: should the cryptographic assumption be a module parameter or an external-mathematics owner row (the echo-types Fidelity idiom)? This PR uses a module parameter, as PROMPT asked. Switching later would only change how unforgeable is supplied.

Governance Impact

  • none beyond the spec status column

Checklist

  • SPDX headers present on every new file
  • AsciiDoc validated (PROOF-NEEDS.adoc, spec)
  • Commit messages follow schema
  • Invisible-character scan clean; shellcheck clean

Additional Context

Gate output (local, Agda 2.6.3):

Agda version 2.6.3
PASS: proofs/agda/Provenance/Warrant.agda
PASS: rejected AssumptionDropped at its invalid declaration
PASS: rejected ConsentFromToken at its invalid declaration
PASS: rejected SignatureToConsent at its invalid declaration
PASS: rejected UnverifiedSignature at its invalid declaration
PASS: control, a typechecking variant of ConsentFromToken is reported as accepted
PASS: Provenance.Warrant and all 4 expected rejections

Negative controls, each run and then reverted:

  • Replacing ConsentFromToken with a valid body fails the gate: invalid proof accepted.
  • Breaking an import in SignatureToConsent fails 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-slim container 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's agda job is the first 2.6.4.3 run of the module.

Status rows moved (PROOF-NEEDS.adoc):

  • WL-3 → PROVEN: SignatureVerify.signature-sound.
  • WL-4 → PROVEN: no-consent-sound, plus the ConsentFromToken falsifier.
  • New WL-7 PROVEN: no-transfer, plus SignatureToConsent.
  • New WL-8 TESTED: UnverifiedSignature.

Stack: #163 A (merged) → C (this) → B1 validator build repair → B2 validator levels and fixture → D pmpl-verify levels.

🤖 Generated with Claude Code

https://claude.ai/code/session_01LET2eHeDbN3b4WuxYjMUX9


Generated by Claude Code

…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
@coderabbitai

coderabbitai Bot commented Oct 14, 2026

Copy link
Copy Markdown
Contributor

Review in Change Stack →

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration
  • Configuration used: Organization UI
  • Review profile: ASSERTIVE
  • Plan: Advanced
  • Run ID: 8c2419e5-1ba2-45ab-8200-0000fdd92287
📥 Commits

Reviewing files that changed from the base of the PR and between 2298cd0 and 08d2a22.

📒 Files selected for processing: 13
  • .github/workflows/warrant.yml
  • .gitignore
  • Justfile
  • PROOF-NEEDS.adoc
  • formats/warrant.ncl
  • proofs/agda/Provenance/Warrant.agda
  • scripts/check-agda.sh
  • scripts/fetch-siblings.sh
  • spec/PROVENANCE-SPEC.adoc
  • tests/reject/AssumptionDropped.agda
  • tests/reject/ConsentFromToken.agda
  • tests/reject/SignatureToConsent.agda
  • tests/reject/UnverifiedSignature.agda
 __________________________________________________
< I want to be a VS Code extension when I grow up. >
 --------------------------------------------------
  \
   \   \
        \ /\
        ( )
      .( o ).
✨ Finishing Touches
📝 Generate docstrings
  • Commit to this branch
  • Create a new PR
  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

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.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

@sonarqubecloud

Copy link
Copy Markdown

@hyperpolymath
hyperpolymath marked this pull request as ready for review October 14, 2026 01:31
@hyperpolymath
hyperpolymath merged commit 0d204db into main Oct 14, 2026
39 of 47 checks passed
@hyperpolymath
hyperpolymath deleted the claude/new-session-8bfbi9 branch October 14, 2026 01:32

Copy link
Copy Markdown
Owner Author

CI on this PR: this PR's own jobs pass. Warrant levels / Provenance.Warrant typechecks; reject fixtures are refused ran on Agda 2.6.4.3, and Warrant records against formats/warrant.ncl passed too.

The red checks are the same set that is red on main at bd13ce7 and was red on #163. None of them involves a file this PR touches:

  • Check SPDX headers (ci.yml): many existing .adoc/.rs files carry MPL-2.0, not PMPL-1.0-or-later. Every new file in this PR carries the PMPL header.
  • governance / Actions lockfile verify: the repo has no .github/workflows/actions.lock, and the grace window closed on 2026-10-01. The fix is to run standards' scripts/update-actions-lock.sh and commit the lockfile. That script is not in this repo, so I haven't done it here.
  • governance / Workflow security linter and Check Workflow Staleness: hypatia-scan.yml and scorecard.yml pin hyperpolymath/standards@7fdc2705df74, which is not reachable from standards' main. scorecard.yml also publishes SARIF directly, which is retired. The fix is to repin both to a commit on standards' main and call scorecard-reusable.yml.
  • scan / gitleaks: all three findings are in .gitleaks-estate.toml, the scanner's own downloaded config, which a --no-git --source . scan picks up. Nothing in this PR is flagged.

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

hyperpolymath added a commit that referenced this pull request Oct 14, 2026
…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>
hyperpolymath added a commit that referenced this pull request Oct 14, 2026
)

## 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>
hyperpolymath added a commit that referenced this pull request Oct 14, 2026
…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>
hyperpolymath added a commit that referenced this pull request Oct 14, 2026
## 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>
hyperpolymath added a commit that referenced this pull request Oct 15, 2026
…-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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants