cairn^973 Captured reply fields go to the Keychain and never to Lean

What it says

For an http request with captures, a 2xx reply whose body is a JSON object with each listed top-level field present once as a string has each value written exactly to its account's Keychain item, and Lean receives the body with each of those values written as an empty string and every other byte as the server sent it; a body that is not a JSON object, or a listed field that is missing, repeated or not a string, answers failed invalid and writes nothing, and a failed write leaves every item as it was. Any other reply passes through unchanged. A captured value appears in no reply, failure message, frame, dump or debug description.

Evidence

assumed	Stated, not proved. The proofs rely on it.
fuzzed	Not shown yet: the trusted-base fuzzer's check `effects.http.capture` held. A CI step will publish it (#95).

Where it's defined

Declaration: Cairn.Fuzz.Trusted.Claims.hostCapture
Module: Cairn.Fuzz.Trusted.Claims
Source: lean/Cairn/Fuzz/Trusted/Claims.lean:132 at v0.5.2
Statement hash: -

Ledger

cairn^973 is active in this version's claims.lock. An id never moves or changes meaning.