Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^27 No request is lost

An invariant of pairs 0.1.3.

Id
pairs^27
Kind
invariant
Reads as
proved
Version
0.1.3

All of pairs 0.1.3's claims

What it says

Every request Pairs makes (manifests, images, the scores file, the packs folder) is answered, cancelled or still awaited, exactly once; ids awaited are distinct and were issued. Cairn's runtime sends at most six network requests at a time and drops replies to cancelled ones.

Evidence

provedinitPairs.noneLost.init
provedstepPairs.noneLost.step
provedreceivePairs.noneLost.receive
provedreachablePairs.noneLost.reachable
provedreachableAllPairs.noneLost.reachableAll
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration
Pairs.noneLost
Module
Pairs.Claims
Source
lean/Pairs/Claims.lean:430 at v0.1.3
Machine
Pairs.machine
Statement
Pairs.noneLost.holds
Statement hash
ac9c05a54e007e8c

Ledger

pairs^27 is active in this version's claims.lock, statement ac9c05a54e007e8c. An id never moves or changes meaning.