Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^972 The Keychain keeps what it was given for this app
An assumption of cairn 0.5.2.
- Id
cairn^972- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
The host's Keychain store keeps one generic password item per account, under the app's service (its bundle identifier), in the login keychain (file-based, not synchronized to iCloud, no access group): reading an account gives the value last written to it, exactly, until it is deleted; writing one account changes no other; forgetSecret deletes the item and answers done, also when there was none; a Keychain secret whose item is missing answers failed notFound. Values never appear in a reply, failure message, frame, dump or debug description.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check effects.secret.keychain held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostKeychain- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:128atv0.5.2- Statement hash
-
Ledger
cairn^972 is active in this version's claims.lock. An id never moves or changes meaning.