Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^974 http sends the request as given, with its secret header, and returns the response as received

An assumption of cairn 0.5.2.

Id
cairn^974
Kind
assume
Reads as
assumed
Version
0.5.2

All of cairn 0.5.2's claims

What it says

http sends the method, URL, headers and body as given, plus for a secret the header scheme ++ value, and answers with the response's status, headers sorted by name and body exactly (captured fields aside, ^973); a missing secret is notFound and sends nothing; a request with a secret never follows a redirect, answering the 3xx; a connection failure is network, no answer in time is timeout, and a non-http URL, a bad method, a header (the secret's too) that could inject another, or an empty account is invalid and sends nothing.

Evidence

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

Where it's defined

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

Ledger

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