Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^960 appendFile adds exactly the bytes at the end, or fails and adds nothing
An assumption of cairn 0.5.2.
- Id
cairn^960- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
appendFile answers done only when the file then holds its old bytes followed by exactly the new ones, creating the file with mode 600 and missing directories; appends from several threads each land whole; a directory, a path under a file, a read-only file and a path that can't name a file fail and leave the file unchanged.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check effects.append-file held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostAppendFile- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:76atv0.5.2- Statement hash
-
Ledger
cairn^960 is active in this version's claims.lock. An id never moves or changes meaning.