Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^1002 readDefault answers the default's value as text

An assumption of cairn 0.5.2.

Id
cairn^1002
Kind
assume
Reads as
assumed
Version
0.5.2

All of cairn 0.5.2's claims

What it says

readDefault answers the value CFPreferences holds for the key in the domain as UTF-8 bytes: a string as it is, a boolean as 1 or 0, a number as its decimal text; a missing value is notFound, any other type and an empty domain or key invalid. It never writes a default.

Evidence

assumedStated, not proved. The proofs rely on it.
fuzzedNot shown yet: the trusted-base fuzzer's check effects.read-default held. A CI step will publish it (#95).

Where it's defined

Declaration
Cairn.Fuzz.Trusted.Claims.hostReadDefault
Module
Cairn.Fuzz.Trusted.Claims
Source
lean/Cairn/Fuzz/Trusted/Claims.lean:210 at v0.5.2
Statement hash
-

Ledger

cairn^1002 is active in this version's claims.lock. An id never moves or changes meaning.