Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^320 Retention never deletes today

An invariant of yap 0.1.0.

Id
yap^320
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

The only day files deleted are ones the host listed that are older than today by the clock; today's is never deleted, whatever retentionDays says (`app_retention_never_today`, `retention_never_today`).

Evidence

provedinitYap.retentionKeepsToday.init
provedstepYap.retentionKeepsToday.step
provedreceiveYap.retentionKeepsToday.receive
provedreachableYap.retentionKeepsToday.reachable
provedreachableAllYap.retentionKeepsToday.reachableAll
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration
Yap.retentionKeepsToday
Module
Yap
Source
lean/Yap.lean:362 at v0.1.0
Machine
Yap.machine
Statement
Yap.retentionKeepsToday.holds
Statement hash
a95e3330ac93a741

Ledger

yap^320 is active in this version's claims.lock, statement a95e3330ac93a741. An id never moves or changes meaning.