Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1009 cancelRequest stops a running request's work; it is still answered once
An assumption of cairn 0.5.2.
- Id
cairn^1009- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
On cancelRequest for a request still running, the host stops its work where it can (an http, upload or loadImage download's URLSession task is cancelled) and still answers it exactly once, failed if the work was stopped, at once if its handler had not started; a cancelled loadImage leaves the image store as it was; a cancel of an id already answered or never requested does nothing.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check effects.cancel held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostCancelRequest- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:240atv0.5.2- Statement hash
-
Ledger
cairn^1009 is active in this version's claims.lock. An id never moves or changes meaning.