Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^323 Too short, silent or nowhere to type: never sent

An invariant of yap 0.1.0.

Id
yap^323
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

Every whole-clip upload is of the recording in progress, at least 0.3 s long, with a sample at or above the silence peak, and with an app to type into (`app_sendable`, `step_transcribe`).

Evidence

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

Ledger

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