Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^29 Only a finished pack changes the board

An invariant of pairs 0.1.3.

Id
pairs^29
Kind
invariant
Reads as
proved
Version
0.1.3

All of pairs 0.1.3's claims

What it says

A reply changes the board only when it is an image answering ready, to a request the pack being loaded made since it began loading: a failure, a pack.json that doesn't parse, a reply for a pack that was switched away from, or any reply while no pack is loading leaves the game as it was.

Evidence

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

Ledger

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