Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^317 Late and cancelled replies never type

An invariant of yap 0.1.0.

Id
yap^317
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

Only a reply to a whole-clip transcription that is still in flight, and was not cancelled since it was sent, types anything; a duplicate, a reply to something else, or a reply after Dictate with Key was turned off types nothing (`app_only_live_replies_type`, `late_reply_never_types`).

Evidence

provedinitYap.onlyLiveRepliesType.init
provedstepYap.onlyLiveRepliesType.step
provedreceiveYap.onlyLiveRepliesType.receive
provedreachableYap.onlyLiveRepliesType.reachable
provedreachableAllYap.onlyLiveRepliesType.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
Yap.onlyLiveRepliesType
Module
Yap
Source
lean/Yap.lean:330 at v0.1.0
Machine
Yap.machine
Statement
Yap.onlyLiveRepliesType.holds
Statement hash
481ca45d51f682ad

Ledger

yap^317 is active in this version's claims.lock, statement 481ca45d51f682ad. An id never moves or changes meaning.