Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^914 The host answers every request exactly once, with its id

An assumption of cairn 0.5.2.

Id
cairn^914
Kind
assume
Reads as
assumed
Version
0.5.2

All of cairn 0.5.2's claims

What it says

Every request the host runs is answered at most once and, when its handler answers, exactly once, under its own id with the handler's first answer; a kind with no handler is answered invalid; after the app starts over no answer to an earlier request is sent.

Evidence

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

Where it's defined

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

Ledger

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