Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^28 A late reply changes nothing

An invariant of pairs 0.1.3.

Id
pairs^28
Kind
invariant
Reads as
proved
Version
0.1.3

All of pairs 0.1.3's claims

What it says

A reply to a request Pairs isn't waiting for (cancelled when a pack switch stopped it, superseded, or a duplicate) leaves everything as it was.

Evidence

provedinitPairs.staleIgnored.init
provedstepPairs.staleIgnored.step
provedreceivePairs.staleIgnored.receive
provedreachablePairs.staleIgnored.reachable
provedreachableAllPairs.staleIgnored.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.staleIgnored
Module
Pairs.Claims
Source
lean/Pairs/Claims.lean:444 at v0.1.3
Machine
Pairs.machine
Statement
Pairs.staleIgnored.holds
Statement hash
7da57f59feb3318b

Ledger

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