Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^311 A shortcut never sends

An invariant of yap 0.1.0.

Id
yap^311
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

While the dictation key is held and another key has gone down with it (a shortcut such as the key plus C), nothing the host reports leads to a clip's upload for transcription: not the key's release, not a new key in config.json, not a reply, and never the menu. Only the clock (or a timer) can, for a hands-free recording that hits its ten-minute limit (`app_shortcut_never_sends`, `shortcut_never_sends`).

Evidence

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

Ledger

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