Claim ยท yap 0.1.0
yap^351 Hold to talk, tap to latch: 300 ms, timed as the original
An invariant of yap 0.1.0.
- Id
yap^351- Kind
- invariant
- Reads as
- proved
- Version
- 0.1.0
What it says
Releasing the key ends a press that began a recording, not part of a shortcut: held for less than 300 ms it was a tap, and the recording goes on hands free with its deadline ten minutes on; held 300 ms or more, the recording ends and is sent (`hold_tap_split`). As in the original, whose main thread is busy in `engine.start()` until the microphone runs, a release that comes while the microphone is starting waits, and is timed from when the start finished, not from its own timestamp: a tap during a slow start (one that ends 300 ms or more after the press) is a hold (`micStarted_replay`).
Evidence
| proved | init | Yap.holdTapSplit.init |
| proved | step | Yap.holdTapSplit.step |
| proved | receive | Yap.holdTapSplit.receive |
| proved | reachable | Yap.holdTapSplit.reachable |
| proved | reachableAll | Yap.holdTapSplit.reachableAll |
| fuzzed | Not shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95). | |
| tested | Not 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.holdTapSplit- Module
Yap- Source
lean/Yap.lean:248atv0.1.0- Machine
Yap.machine- Statement
Yap.holdTapSplit.holds- Statement hash
56e714e3634ee4c5
Ledger
yap^351 is active in this version's claims.lock, statement 56e714e3634ee4c5. An id never moves or changes meaning.