Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^967 A clip's WAV for a range of windows holds exactly those samples
An assumption of cairn 0.5.2.
- Id
cairn^967- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
An upload's wav part for clip c and windows s to e is a 16 kHz mono 16-bit RIFF/WAVE file of exactly samples 320 s to 320 e of the clip (to the end of the clip when e is none, waiting for a clip whose recording is being stopped); a range past the end or backwards is invalid, an unknown or forgotten clip notFound, and forgetClip answers done once and notFound after.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check effects.clip-wav held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostClipWav- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:108atv0.5.2- Statement hash
-
Ledger
cairn^967 is active in this version's claims.lock. An id never moves or changes meaning.