Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^970 upload sends the body assembled from its parts, with the secret in its header

An assumption of cairn 0.5.2.

Id
cairn^970
Kind
assume
Reads as
assumed
Version
0.5.2

All of cairn 0.5.2's claims

What it says

upload sends one request whose body is its parts in order, each wav part replaced by the clip's WAV, with its headers and, for a secret, the header scheme ++ value; a missing clip, bad range or missing secret fails before anything is sent; otherwise it answers as http does.

Evidence

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

Where it's defined

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

Ledger

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