Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^346 The original Yap keeps its key

An invariant of yap 0.1.0.

Id
yap^346
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

Yap (Cairn) takes the dictation key only once it has checked that the original Yap (dev.yap.Yap) is not running: while it runs, or before the check is answered, there is no global key subscription, and the menu says so (`wantsKey`).

Evidence

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

Ledger

yap^346 is active in this version's claims.lock, statement 57714dd87b738fea. An id never moves or changes meaning.