Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^347 A mark waits for the appends

An invariant of yap 0.1.0.

Id
yap^347
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

Yap marks a typed transcript's line in its day file (`"typed":true`) by rewriting the file, and the host runs requests concurrently, so a line is only known to be there once its append is answered. The app keeps the day-file appends it has sent and not heard back from (`Io.appends`): every append it sends is kept, with its line, and one leaves only when a reply with its id arrives; a line is saved for marking only when the reply to its append says it worked; and a mark's read goes out only for a saved line, when no append is in flight after the message, so never before its own append is answered nor in the same frame as another. The menu starts no mark and drops no append (`receive_tracks`, `receive_answers`, `receive_saves`, `receive_marks`, `menuStep_marks`). That a typed transcript then ends up marked on disk is fuzzed, not proved (`yapfuzz`, app mode).

Evidence

provedinitYap.markAfterAppend.init
provedstepYap.markAfterAppend.step
provedreceiveYap.markAfterAppend.receive
provedreachableYap.markAfterAppend.reachable
provedreachableAllYap.markAfterAppend.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.markAfterAppend
Module
Yap
Source
lean/Yap.lean:404 at v0.1.0
Machine
Yap.machine
Statement
Yap.markAfterAppend.holds
Statement hash
7e071a0a92c80734

Ledger

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