Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^966 record streams the levels of exactly the samples it keeps, and nothing after its stop
An assumption of cairn 0.5.2.
- Id
cairn^966- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
While a record subscription runs, its audio events count every sample the clip keeps, in order, and their windows are the 20 ms levels (sum of squares and peak of each 320 samples) of those samples from the start of the clip, however the microphone split them; after its stop has been handled none is sent and the clip is finished; a microphone that can't start (no permission, no device) is one failed event and an empty clip, and the microphone is never started without the permission.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check subs.record held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostRecord- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:100atv0.5.2- Statement hash
-
Ledger
cairn^966 is active in this version's claims.lock. An id never moves or changes meaning.