Cairn Docs Claims Blog Packages

Claim ยท cairn 0.3.0

cairn^1001 appRunning answers whether an app with that bundle id runs

An assumption of cairn 0.3.0.

Id
cairn^1001
Kind
assume
Reads as
assumed
Version
0.3.0

All of cairn 0.3.0's claims

What it says

appRunning answers flag true exactly when the system lists a running, not terminated app with that bundle identifier; an empty identifier is invalid.

Evidence

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

Where it's defined

Declaration
Cairn.Fuzz.Trusted.Claims.hostAppRunning
Module
Cairn.Fuzz.Trusted.Claims
Source
lean/Cairn/Fuzz/Trusted/Claims.lean:182 at v0.3.0
Statement hash
-

Ledger

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