docs: stop duplicating the lib.pvl digest in REPRODUCING.md

The doc quoted an expected SHA-256 of
51b54eed55ee23d19386f7a62fb68dbf3a25ef80d5567c77f86e1c8d20f6395b, but the real
digest of the committed extraction/lib.pvl -- and the value in
extraction/lib.pvl.sha256 -- is
4914798cd53878dec1b3f43a00dad9d322013cd0cc09f14e7634e6366c70572c. The prose
copy had gone stale.

Nothing was actually wrong with the extraction: the L2 recipe checks the
.sha256 file, not the doc, so it kept passing. But anyone eyeballing
REPRODUCING.md would conclude the extraction had drifted when it had not --
which is a bad failure mode for a document whose whole job is to certify
byte-identity.

Point at extraction/lib.pvl.sha256 instead of restating the value. That file is
regenerated alongside lib.pvl, so it cannot drift, and it is what `shasum -c`
already verifies. Repeating the digest next to the file that holds it is what
caused this, so the fix removes the duplication rather than refreshing it.

Author: karthikbhargavan

proofs/proverif/REPRODUCING.md

@@ -117,9 +117,16 @@ python3 hax.py extract-proverif                 # regenerate extraction/lib.pvl
 shasum -a 256 -c proofs/proverif/extraction/lib.pvl.sha256   # must match
 ```
 
-Expected `lib.pvl` digest (SHA-256):
-`51b54eed55ee23d19386f7a62fb68dbf3a25ef80d5567c77f86e1c8d20f6395b`
-(also stored in `extraction/lib.pvl.sha256`).
+The expected `lib.pvl` digest (SHA-256) lives in `extraction/lib.pvl.sha256`,
+which is what the `shasum -c` above checks. Read it with:
+
+```bash
+cat proofs/proverif/extraction/lib.pvl.sha256
+```
+
+That file is the single source of truth: it is regenerated alongside `lib.pvl`,
+so it cannot drift. Do not copy the digest into prose here — an earlier copy
+went stale and made the extraction look like it had drifted when it had not.
 
 ### Regression (the SPQR refactors are behaviour-preserving)