cairn^1006 loadImage answers the image's pixel size, or the fault

What it says

loadImage of a file path (~/ is home, relative to the working directory) or an http(s) URL decodes the first image with ImageIO, applying its EXIF orientation, keeps it for image draws naming the same source and answers image with the oriented pixel size, exactly once; a missing file is notFound, an unreadable one denied, a directory, an empty source, NUL or bytes that are no image invalid; HTTP 404 and 410 notFound, 401 and 403 denied, any other status outside 2xx other, a failed connection network, a timeout timeout. Without reload a kept source is answered from the store without reading; with reload it is read again, and a failure removes it.

Evidence

Where it's defined

Declaration

Cairn.Fuzz.Trusted.Claims.hostLoadImage

Module

Cairn.Fuzz.Trusted.Claims

Source

lean/Cairn/Fuzz/Trusted/Claims.lean:226 at v0.5.2

Statement hash

-

Ledger

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